fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Add always_invert_Some	Jason Gross	2018-02-17
\|
*	Add a file to parse taps with Coq notations	Jason Gross	2018-02-14
\|
*	Add some string utility functions	Jason Gross	2018-02-13
\|
*	Add expand_list_correct to ListUtil	Jason Gross	2018-02-12
\|
*	Add string conversions	Jason Gross	2018-02-11
\|
*	Add notation for option_bind	Jason Gross	2018-02-10
\|
*	Split off ZRange lemmas	Jason Gross	2018-02-10
\|
*	Add some ZRange operations	Jason Gross	2018-02-10
\|
*	minor updates needed to make it compile with bbv	Samuel Gruetter	2018-02-05
\| \| \| \|	removing lemma wordToNat_wzero is ok because it's already in bbv
*	Add better levels / printing for bind notations	Jason Gross	2018-01-16
\|
*	Add a comment for why Z.peano_rect_strong exists.	David Benjamin	2018-01-14
\|
*	Factor out fsatz lemmas	Jason Gross	2018-01-09
\| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change \| % Change ------------------------------------------------------------------------- 1m11.42s \| Total \| 1m53.75s \|\| -0m42.33s \| -37.21% ------------------------------------------------------------------------- 1m06.02s \| Curves/Weierstrass/Jacobian \| 1m53.76s \|\| -0m47.73s \| -41.96% 0m05.40s \| Util/FsatzAutoLemmas \| N/A \|\| +0m05.40s \| ∞
*	Add @@ infix notation	Jason Gross	2018-01-06
\|
*	Add some reserved notations for cps stuff	Jason Gross	2017-12-27
\|
*	Add pow_ceil_mul_nat_divide_nonzero	Jason Gross	2017-12-15
\|
*	Add reserved notation for infix @ for application	Jason Gross	2017-12-15
\|
*	Add fast-path versions of [destruct_head] for unit,bool,True	Jason Gross	2017-12-12
\|
*	Rename run_tactic_as_bool to is_success_run_tactic	Jason Gross	2017-11-26
\| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153084144
*	Reserve a printing-only notation for function application	Jason Gross	2017-11-26
\| \| \| \|	This sets the level and associativity in a common place, and will be useful for PHOAS application nodes
*	Add Tactics.RunTacticAsConstr	Jason Gross	2017-11-26
\|
*	Add reserved expr_let notation	Jason Gross	2017-11-26
\|
*	Add support for custom intro tactic in ring pkg, for speed	Jason Gross	2017-11-17
\|
*	Add fast path for vm_decide (_ = false)	Jason Gross	2017-11-17
\|
*	Add fast path for vm_decide (_ = true) package	Jason Gross	2017-11-17
\|
*	Add native_compute evar packages	Jason Gross	2017-11-16
\|
*	Add vm_compute_cbv_evar_package	Jason Gross	2017-11-16
\|
*	Add ModInv autosolver	Jason Gross	2017-11-16
\|
*	Make pipeline options more easily extensible	Jason Gross	2017-11-13
\| \| \| \| \|	Also add a dummy option about renaming binders, to be used in an upcoming commit.
*	Add autosolve admit package	Jason Gross	2017-11-12
\|
*	Use abstract in ring autosolve	Jason Gross	2017-11-12
\|
*	Add Decidable2Bool	Jason Gross	2017-11-11
\|
*	Add ListUtil.Forall	Jason Gross	2017-11-11
\|
*	First intro and split in Zring_prod_eq_tac, before cbv -	Jason Gross	2017-11-11
\|
*	More modularity in autosolve	Jason Gross	2017-11-10
\|
*	Separate case for handling option matches in autosolve	Jason Gross	2017-11-10
\|
*	Add cbn [val] in autosolve	Jason Gross	2017-11-10
\|
*	Fix opacity of dec_Forall, dec_Exists	Jason Gross	2017-11-10
\|
*	Add dec_if_bool	Jason Gross	2017-11-10
\|
*	Generalize Tuple.dec_fieldwise	Jason Gross	2017-11-09
\|
*	Generalize Forall2_forall_iff	Jason Gross	2017-11-09
\|
*	More generalization of fieldwise'_Proper to dependent types	Jason Gross	2017-11-09
\|
*	Generalize fieldwise Proper lemmas	Jason Gross	2017-11-09
\|
*	Add fieldwise_lift_and	Jason Gross	2017-11-09
\|
*	Add more versions of fieldwise_Proper	Jason Gross	2017-11-09
\|
*	Add fieldwise_Proper	Jason Gross	2017-11-09
\|
*	Add fieldwise_eq_iff	Jason Gross	2017-11-09
\|
*	Add dec_Forall, dec_Exists	Jason Gross	2017-11-09
\|
*	Add fieldwise_map_from_list_iff	Jason Gross	2017-11-09
\|
*	Add option_map_map	Jason Gross	2017-11-07
\|
*	Add Tuple.dec_eq{,'}	Jason Gross	2017-11-07
\|