fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix 8.4 build.	jadep	2016-07-25
\|
*	A couple new util lemmas	jadep	2016-07-25
\|
*	Add another lemma about +, <= to arith	Jason Gross	2016-07-20
\|
*	Fix for Coq 8.4 (omega used to be weaker)	Jason Gross	2016-07-18
\|
*	Add more natsimplify le_dec lemmas	Jason Gross	2016-07-18
\|
*	Add more NatUtil lemmas	Jason Gross	2016-07-18
\|
*	Add natsimplify lemmas about eq_nat_dec	Jason Gross	2016-07-18
\|
*	Added lemmas to ZUtil and NatUtil (for Testbit)	jadep	2016-07-18
\|
*	Fix NatUtil for 8.4	Jason Gross	2016-07-08
\|
*	Add useful tactics and util lemmas	Jason Gross	2016-07-08
\|
*	Add a NatUtil lemma and db	Jason Gross	2016-07-08
\|
*	Fix ListUtil for Coq 8.4	Jason Gross	2016-07-07
\|
*	Add [update_nth] to ListUtil, change [set_nth]	Jason Gross	2016-07-06
\| \| \| \|	Define [set_nth] in terms of [update_nth]
*	Prove that a ^ k <> 0	Jason Gross	2016-06-30
\|
*	Merge	jadep	2016-06-14
\|\
* \|	progress on second stage (conditional constant-time subtraction) of ↵	jadep	2016-06-13
\| \| \| \| \| \| \| \|	canonicalization proofs
\| *	8.5 fixes	Jason Gross	2016-06-10
\|/
*	moved lemmas from ModularBaseSystemProofs to various Util files	jadep	2016-04-20
\|
*	Finish absolutizing imports	Jason Gross	2016-03-10
\| \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	a few lemmas in util about powers of 2 in Bedrock's various rewritten forms	Jade Philipoom	2016-02-15
\|
*	Util: added util lemmas needed to instantiate EdDSA25519.	Jade Philipoom	2016-01-05