fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Coq 8.5 can't handle symbol-free notations	Jason Gross	2017-10-06
\|
*	Clean up TestCase a bit	Jason Gross	2017-10-06
\|
*	Don't rely on autogenerated names	Jason Gross	2017-06-05
\| \| \| \| \| \|	This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
*	CSE without inlining arithmetic expressions	Jason Gross	2017-05-14
\| \| \| \| \| \| \| \| \| \|	This takes care of most of #158. The remaining bits are reworking the Wf and interpretation lemmas to actually work. (The former needs a only bit of rethinking and rephrasing to handle the fact that sometimes we change the stored symbolic expression from a complicated one to a fresh variable, while the latter needs major surgery, which Adam tells me is easy, and this is a note that when I come back to it, I should look at the email thread with Adam about CSE from last summer.)
*	Split off a-normal form from flattening	Jason Gross	2017-04-14
\| \| \| \|	Now we can flatten let binders without putting operations in a-normal form
*	Add support for cse-modulo-normalization	Jason Gross	2017-04-14
\|
*	Split off Compilers.Named.Context	Jason Gross	2017-04-10
\|
*	Merge branch 'rename-everything'. Closes #14.	Andres Erbsen	2017-04-06
\|
*	rename-everything	Andres Erbsen	2017-04-06