fiat-crypto - fast, formally verified cryptography

	Commit message (Expand)	Author	Age
...
* \|	Removed lingering print statement.	jadep	2016-07-21
\| *	Faster update-_CoqProject target	Jason Gross	2016-07-21
\| *	Fix clean target	Jason Gross	2016-07-21
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-21
\|\\|
* \|	Fixes #29	jadep	2016-07-21
* \|	re-introduced extra field isomorphism layer for 8.4 compatibility and better ...	jadep	2016-07-21
\| *	ed25519 spec: small cleanup	Andres Erbsen	2016-07-21
\| *	Add support for TIMED=1 in Coq 8.4	Jason Gross	2016-07-20
\| *	Don't depend on the submodule; copy-paste instead	Jason Gross	2016-07-20
\| *	Add a separate non-specific target	Jason Gross	2016-07-20
\| *	Merge pull request #33 from JasonGross/dir-locals	Andres Erbsen	2016-07-20
\| \|\
\| * \|	automate a proof	Andres Erbsen	2016-07-20
\| * \|	compute on [F q]!	Andres Erbsen	2016-07-20
\| * \|	experiments wd25519: simplify proof for a	Andres Erbsen	2016-07-20
\| \| *	Add target for .dir-locals.el	Jason Gross	2016-07-20
\| \|/
* \|	Merge branch 'master' of github.com:mit-plv/fiat-crypto	jadep	2016-07-20
\|\\|
* \|	merge	jadep	2016-07-20
\|\ \
\| \| *	Move mul_rep_extended (do we actually care about this?)	Jason Gross	2016-07-20
\| \|/
\| *	Don't use auto with *	Jason Gross	2016-07-20
* \|	restructured ModularBaseSystem pipeline to put tuple conversion before Modula...	jadep	2016-07-20
\| *	Absolutize some imports	Jason Gross	2016-07-20
\| *	Silence a deprecation warning	Jason Gross	2016-07-20
\| *	Display pretty timing graph on travis	Jason Gross	2016-07-20
\| *	Remove dependency of ext_base on pseudomersenne	Jason Gross	2016-07-20
\| *	Add Z.lt_le_incl to zarith	Jason Gross	2016-07-20
\| *	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
\| *	Use a proof that doesn't require as many assumptions in extended_base_length	Jason Gross	2016-07-20
\| *	Work around bad design in Coq	Jason Gross	2016-07-19
\| *	Add a distr_length database	Jason Gross	2016-07-19
\| *	Remove stuff from PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| *	{base} -> base	Jason Gross	2016-07-19
\| *	Move two_k_nonzero to PseudoMersenneBaseParamProofs.v	Jason Gross	2016-07-19
\| *	Fix side-condition from previous commit	Jason Gross	2016-07-19
\| *	Add another lemma to distr_length	Jason Gross	2016-07-19
* \|	merge	jadep	2016-07-19
\|\\|
* \|	Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.	jadep	2016-07-19
\| *	Use update_nth in add_to_nth (#26)	Jason Gross	2016-07-19
\| *	Bump submodule	Jason Gross	2016-07-19
\| *	Bump submodule	Jason Gross	2016-07-19
* \|	merge	jadep	2016-07-19
\|\ \
\| \| *	ext_base: now defined in terms of ext_limb_widths	Jason Gross	2016-07-18
\| \| *	Add a lemma about base_from_limb_widths and app	Jason Gross	2016-07-18
\| \| *	Add a lemma about sum_firstn	Jason Gross	2016-07-18
\| \| *	Add a ListUtil lemma	Jason Gross	2016-07-18
\| \| *	Move more proofs earlier	Jason Gross	2016-07-18
\| \| *	Make Pow2BaseProofs independent of the def of add_to_nth	Jason Gross	2016-07-18
\| \| *	Silence a warning	Jason Gross	2016-07-18
\| \| *	Express carry_simple in terms of carry_gen	Jason Gross	2016-07-18
\| \| *	Fix for Coq 8.4 (missing lemmas)	Jason Gross	2016-07-18
\| \| *	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18