fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add a classification of n / m < 0	Jason Gross	2016-06-30
\|
*	Add a tactic for making use of destructed <? in Z	Jason Gross	2016-06-30
\|
*	Prove that a ^ k <> 0	Jason Gross	2016-06-30
\|
*	Add pow_Zpow to Util.ZUtil	Jason Gross	2016-06-30
\| \| \| \|	I followed the naming scheme of things like div_Zdiv in the stdlib.
*	Simplify conservative_common_denominator	Jason Gross	2016-06-29
\| \| \| \| \| \| \| \| \| \| \|	We no longer try to predict field_simplify_eq. This results in better behavior and less code which is more modular. In particular, the tactic responsible for hiding non-fraction pieces from field_simplify_eq no longer tries to preemptively assert that denominators are nonzero. This improvement is a result of @andres-erbsen's point in #16, https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69035102 , that we were generating too many side-conditions.
*	Don't generate goals [False] in conservative_common_denominator_all	Jason Gross	2016-06-29
\| \| \| \|	See also #16, https://github.com/mit-plv/fiat-crypto/pull/16/files/f1744181ad236300cfa9ba7c033684fbdf45a3e9..4e50ef26b9b02c882536281e1c7a0cf013a963d5#r69034941
*	Fix [only_two_square_roots] to not loop	Jason Gross	2016-06-29
\| \| \| \| \|	It was previously posing hypotheses that were algebraic duplicates of existing hypotheses, and then clearing them.
*	Allow side-conditions in common denom. all in hyps	Jason Gross	2016-06-29
\| \| \| \| \|	This should handle #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009840
*	Handle fractions in denominators	Jason Gross	2016-06-29
\| \| \| \| \|	This should deal with #16 / https://github.com/mit-plv/fiat-crypto/pull/16#discussion_r69009776
*	Clear symmetric duplicates in clear_algebraic_duplicates	Jason Gross	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Update crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Create crypto-defects.md	Andres Erbsen	2016-06-29
\|
*	Fix a typo in the previous commit	Jason Gross	2016-06-28
\|
*	[super_nstaz]: Handle side-conditions from [nsatz]	Jason Gross	2016-06-28
\|
*	Revert "CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge"	Andres Erbsen	2016-06-28
\| \| \| \|	This reverts commit 4ab9da1b82913f1ad798bcdacd8801f619ee2fdf.
*	No more anomalies from super_nsatz, hopefully	Jason Gross	2016-06-28
\|
*	Fix field_algebra in 8.4	Jason Gross	2016-06-28
\|
*	CompleteEdwardsCurveTheorems: build on 8.4 after field_algebra cahnge	Andres Erbsen	2016-06-28
\|
*	Also install libcoq-ocaml	Jason Gross	2016-06-28
\| \| \| \| \|	Because I can't figure out how to package coq so that coq depends on libcoq-ocaml automatically.
*	Add many versions of Coq 8.4 to travis	Jason Gross	2016-06-28
\|
*	Fix a typo (missing .)	Jason Gross	2016-06-28
\|
*	Fix super_nsatz tactic to be better about ordering	Jason Gross	2016-06-28
\| \| \| \|	See also #13.
*	EdDSARefinement: work around rewrite_strat for 8.4	Andres Erbsen	2016-06-28
\|
*	Tuple: from_list_to_list	Andres Erbsen	2016-06-28
\|
*	Try a faster way of solving some inequalities resulting from common_denominator	Jason Gross	2016-06-27
\|
*	Actual fix for super_nsatz	Jason Gross	2016-06-27
\|
*	Fix super_nstaz to not error	Jason Gross	2016-06-27
\|
*	Add a super_nsatz tactic	Jason Gross	2016-06-27
\|
*	eddsa refinement setup	Andres Erbsen	2016-06-27
\|
*	Add [destruct_head] tactics	Jason Gross	2016-06-27
\|
*	Update .mailmap with email from 3c36b589a01bce19063872544bca132f3daf947d	Jason Gross	2016-06-27
\|
*	Merge pull request #9 from mit-plv/folkwisdom	Andres Erbsen	2016-06-27
\|\ \| \| \| \|	Document "folk wisdom" tips that would have been good to know
\| *	Update folkwisdom.md	Andres Erbsen	2016-06-27
\| \|
* \|	Add [break_match] for hypotheses	Jason Gross	2016-06-27
\| \|
* \|	Update .gitignore	Jason Gross	2016-06-27
\| \|
* \|	Add decidable instances for sumwise and fieldwise	Jason Gross	2016-06-27
\| \|
* \|	Add a tactic for dealing with equalities of [sum]	Jason Gross	2016-06-27
\| \|
* \|	Fix notation level	Jason Gross	2016-06-27
\| \|
* \|	Add global notation for eq_dec	Jason Gross	2016-06-27
\| \|