fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
*	Merge pull request #84 from mit-plv/rsloan-phoas	Jason Gross	2016-10-27
\|\
* \|	prove admit about F.to_nat x mod m	Andres Erbsen	2016-10-27
* \|	proved last admit (Proper_feEnc) in Experiments/Ed25519	jadep	2016-10-27
* \|	proved an admit (eq_enc_S_iff) in Ed25519.v	jadep	2016-10-27
* \|	Add Inline import	Jason Gross	2016-10-27
* \|	Add {un,}curry_wire_digits	Jason Gross	2016-10-27
* \|	CompleteEdwardsCurve.ExtendedCoordinates: remove admitted lift_homomorphism l...	Andres Erbsen	2016-10-27
* \|	Add {un,}curry_{bin,un}op_fe25519	Jason Gross	2016-10-27
* \|	Add length_fe25519	Jason Gross	2016-10-27
* \|	Fix implicit status of curry	Jason Gross	2016-10-27
* \|	Add curry and uncurry to tuple	Jason Gross	2016-10-27
* \|	Add syntax and reification for the ops in GF25519	Jason Gross	2016-10-27
* \|	Fix a missing import in previous commit	Jason Gross	2016-10-27
* \|	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
* \|	PHOAS notation fixups	Jason Gross	2016-10-27
* \|	Make it easier to export only phoas notations	Jason Gross	2016-10-27
* \|	add wf, not only rel_wf, to MapInterpWf	Jason Gross	2016-10-27
* \|	Add WfRelReflective	Jason Gross	2016-10-27
* \|	Factor WfReflective through WfReflectiveGen	Jason Gross	2016-10-27
* \|	removed now irrelevant commented-out code	jadep	2016-10-27
* \|	convert feEnc correctness proof to bounded type	jadep	2016-10-27
* \|	finished feEnc correctness	jadep	2016-10-27
* \|	most of feEnc correctness proof	jadep	2016-10-27
* \|	Slightly loosen freeze preconditions (in particular, I had failed to properly...	jadep	2016-10-27
* \|	add extra convenience lemmas about boundedness of convert	jadep	2016-10-27
* \|	removed lingering TODO	jadep	2016-10-27
* \|	Implicits for reflect_wfT	Jason Gross	2016-10-27
* \|	Add WfReflectiveGen	Jason Gross	2016-10-27
* \|	Move interp_flat_type_gen_rel_pointwise2 to Syntax	Jason Gross	2016-10-27
* \|	Add Wf proofs about MapInterp	Jason Gross	2016-10-27
* \|	Add arguments to mapf_interp_flat_type_gen	Jason Gross	2016-10-27
* \|	Add implicits to interp_flat_type_gen_rel_pointwise2	Jason Gross	2016-10-27
* \|	Change the argument implicits on rel_wff	Jason Gross	2016-10-27
\| *	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\| \|\ \| \|/ \|/\|
* \|	Revert change to [nsatz] (it was making Coq run out of memory)	Jason Gross	2016-10-27
\| *	Merge branch 'master' into rsloan-phoas	Jason Gross	2016-10-27
\| \|\
* \| \|	Simplify proof of proj1_fe25519_encode	Jason Gross	2016-10-27
* \| \|	Add lemmas about GF25519BoundedCommon.{encode,decode}	Jason Gross	2016-10-27
\| \|/ \|/\|
\| *	Fixes for Coq 8.4	Jason Gross	2016-10-27
\| *	Strip function extensionality, enable printing of sub, mul, opp, freeze	Jason Gross	2016-10-27
* \|	Various fixes in alternative nsatz	Jason Gross	2016-10-27
\| *	Tactics to manually remove Z.to/of_N and such	Robert Sloan	2016-10-26
* \|	Handle folded [not] in nsatz_strip_fractions	Jason Gross	2016-10-26
* \|	Split inequalities before specializing	Jason Gross	2016-10-26
* \|	Fix nsatz: don't clear inequalities	Jason Gross	2016-10-26
* \|	Fix a missing case in generalize_inv	Jason Gross	2016-10-26
* \|	Fix typos	Jason Gross	2016-10-26
* \|	Add tactics to implement better fraction removal	Jason Gross	2016-10-26
* \|	Add lemmas about algebra	Jason Gross	2016-10-26
\| *	Refactors to remove intermediate conversions	Robert Sloan	2016-10-26