fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix for 8.8	Jason Gross	2019-04-05
\|
*	Add interp_related lemmas	Jason Gross	2019-04-05
\|
*	Add some more underlets lemmas	Jason Gross	2019-04-04
\|
*	Add UnderLets flat_map interp proofs,other changes	Jason Gross	2019-04-04
\| \| \| \| \| \| \| \|	Also remove a rewrite rule using cast from the non-cast arith rules, regenerate the .out files, add ident.gets_inlined for eventual use in the rewriter, and generalize the rewrite rule lemmas over cast_out_of_range so that we can actually make use of their proofs for interp.
*	Add UnderLets.wf_flat_map	Jason Gross	2019-03-12
\|
*	Add UnderLets.wf_of_expr	Jason Gross	2019-03-09
\|
*	Add some UnderLets wf proofs	Jason Gross	2019-03-08
\| \| \| \| \| \|	Actually useful ones, this time Constructed with much pain and some trial-and-error and guessing.
*	Standardize list wf things	Jason Gross	2019-03-08
\| \| \| \| \| \| \| \|	Rather than using Forall2 in some places and a combination of length, combine, and In in others, we now primarily use Forall2. There is probably some dead tactic code as a result of this that I just haven't bothered to clean up.
*	Add wf proofs to UnderLetsProofs	Jason Gross	2019-03-07
\|
*	Fix hypothesis of UnderLets.list_rect_arrow_interp_related	Jason Gross	2019-03-07
\|
*	Add UnderLets.list_rect_arrow_interp_related	Jason Gross	2019-03-07
\|
*	Update a proof to work with previous commit	Jason Gross	2019-02-27
\|
*	Add support for reifying `zrange` and `option`	Jason Gross	2019-02-18
\| \| \| \|	This is needed to reify statements for the rewriter.
*	Add Option.{lift,map,combine}, List.Option.lift	Jason Gross	2019-02-11
\| \| \| \|	These will be useful for extending the AST with `option` types.
*	move src/Experiments/NewPipeline/ to src/	Andres Erbsen	2019-01-09