adampetcher

Thanks for the response. These are only suggestions based on my analysis of CVE-2016-5548. Feel free to resolve/close this issue at any time. I see your point about the large...

This is likely a good idea, but making definitions transparent tends to cause problems when they are used. At least, it used to cause problems in older versions of Coq....

I'm not opposed to the idea, but I don't know if there is enough justification, as required by the inclusion criteria. I'm not even aware if anyone has used it...

Thanks for the info! I'm still not opposed to the idea, but I'm not willing to be the maintainer. So I think we will need a volunteer for this part.

1 and 3 are essentially done. I will leave this ticket open to clean up all the source files when I am confident that it won't interfere with other changes.