fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add constr_fail and constr_fail_with	Jason Gross	2019-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \|	Rather than taking the convention that failures during constr construction emit a type error from `I : I` with the actual error message `idtac`d above them (because Coq has no way to emit multiple things on stderr), we instead factor everything through a new `constr_fail` or `constr_fail_with msg_tac`, which emit more helpful messages instructing the user to look in `coq` or to use `Fail`/`try` to see the more informative error message. When we can make our own version that does both `idtac` and `fail` (c.f. https://github.com/coq/coq/issues/3913), then we can do something a bit more sane, hopefully.
*	Fix issue with previous commit	Jason Gross	2019-03-08
\|
*	Add some eq list_rect lemmas to ListUtil	Jason Gross	2019-03-08
\|
*	Add some eq lemmas to ListUtil	Jason Gross	2019-03-07
\|
*	Add some Proper lemmas to ListUtil	Jason Gross	2019-03-07
\|
*	Add remove_duplicates	Jason Gross	2019-01-24
\|
*	prove [eval_conditional_sub]	jadep	2018-12-21
\|
*	Add Forall2_update_nth	Jason Gross	2018-12-06
\|
*	Remove ListUtil.List.repeat	Jason Gross	2018-12-04
\| \| \| \| \|	We are no longer checking against Coq 8.5, and it's simpler to not have two versions of `List.repeat` floating around.
*	Add map_repeat, map_const	Jason Gross	2018-11-11
\|
*	Add some natutil and listutil lemmas	Jason Gross	2018-10-10
\|
*	Add map_update_nth_ext	Jason Gross	2018-10-09
\|
*	Add some util lemmas	Jason Gross	2018-08-13
\|
*	Add ListUtil.map_nth_default_seq	Jason Gross	2018-08-10
\|
*	Add ListUtil.{combine_repeat,combine_rev_rev_samelength}	Jason Gross	2018-08-09
\|
*	Add nth_error_combine	Jason Gross	2018-08-01
\|
*	Add more proper instances	Jason Gross	2018-07-26
\|
*	Add ListUtil.{take,drop}_while	Jason Gross	2018-07-24
\|
*	Add minor lemmas to util	Jason Gross	2018-07-17
\|
*	Add ZUtil, list lemmas	Jason Gross	2018-07-02
\|
*	Fix a notation issue in previous commit	Jason Gross	2018-07-02
\|
*	Add more ListUtil proofs	Jason Gross	2018-07-02
\|
*	Add some list lemmas	Jason Gross	2018-07-02
\|
*	Add useful list lemmas	Jason Gross	2018-06-29
\|
*	Add list_beq	Jason Gross	2018-06-22
\|
*	Add seq_add, seq_len_0	Jason Gross	2018-06-19
\|
*	Move function argument out of fixpoint of List.map2	Jason Gross	2018-05-21
\| \| \| \| \|	This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now.
*	add a list lemma	Jade Philipoom	2018-04-11
\|
*	pass-through after Andres's review in #334	Jade Philipoom	2018-04-03
\|
*	move some lemmas to ZUtil/ListUtil	Jade Philipoom	2018-04-03
\|
*	move some lemmas/hints to ListUtil	Jade Philipoom	2018-04-03
\|
*	Add list_case, a definition for match on list	Jason Gross	2018-03-27
\|
*	add two proofs about lists	Jade Philipoom	2018-02-23
\|
*	Strip the pointed instance names off of the default value in list expansion	Jason Gross	2018-02-18
\| \| \| \|	This is required for reification to work, it seems
*	Add expand_lists tactic	Jason Gross	2018-02-18
\|
*	Add expand_list_correct to ListUtil	Jason Gross	2018-02-12
\|
*	Generalize Forall2_forall_iff	Jason Gross	2017-11-09
\|
*	src/Demo.v: a 200-line introduction to BaseSystem ideas	Andres Erbsen	2017-06-21
\|
*	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).
*	s/appcontext/context/	Jason Gross	2017-05-11
\| \| \| \|	They mean the same thing since 8.5, and appcontext is deprecated.
*	do not use VerdiTactics in files we plan to keep	Andres Erbsen	2017-04-06
\|
*	Add [Proof using] to most proofs	Jason Gross	2017-04-04
\| \| \| \| \| \| \| \|	This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
*	Add lemmas needed for saturated arithmetic [compact]	jadep	2017-03-24
\|
*	Add {firstn,skipn}_seq	Jason Gross	2017-03-19
\|
*	generalize In_firstn_skipn_split	Jason Gross	2017-03-19
\|
*	Add In_firstn_skipn_split	Jason Gross	2017-03-19
\|
*	Add firstn_firstn_min	Jason Gross	2017-03-19
\|
*	Fix a name clash	Jason Gross	2017-03-14
\|
*	Add firstn_skipn	Jason Gross	2017-03-14
\|
*	Add skipn_skipn	Jason Gross	2017-03-14
\|