fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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 Zdiv_0_l to zsimplify dbs	Jason Gross	2018-03-27
\|
*	Add list_case, a definition for match on list	Jason Gross	2018-03-27
\|
*	Add another reserved notation for App_fst	Jason Gross	2018-03-21
\|
*	Don't use deprecated compat notations in ZUtil	Jason Gross	2018-03-07
\|
*	git submodule update --remote --recursive	Andres Erbsen	2018-02-24
\|
*	coqprime in COQPATH (closes #269)	Andres Erbsen	2018-02-24
\|
*	Add ZRange.intersection	Jason Gross	2018-02-23
\|
*	Fix a typo	Jason Gross	2018-02-23
\|
*	Add some bounds operations to ZRange	Jason Gross	2018-02-23
\|
*	Add ZRange.opp	Jason Gross	2018-02-23
\|
*	move things from ZUtil.v into Div.v	Jade Philipoom	2018-02-23
\|
*	add three proofs to ZUtil	Jade Philipoom	2018-02-23
\|
*	add two proofs about lists	Jade Philipoom	2018-02-23
\|
*	add proof about Z.equiv_modulo	Jade Philipoom	2018-02-23
\|
*	create rewrite database for saturated operations on Z	Jade Philipoom	2018-02-23
\|
*	Add new modular addition operation on Z	Jade Philipoom	2018-02-23
\|
*	NumTheoryUtil: make coqprime dependencies explicit	Andres Erbsen	2018-02-19
\|
*	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 pointed types	Jason Gross	2018-02-18
\| \| \| \|	For filling in default values
*	Fix a proof for Coq 8.7	Jason Gross	2018-02-17
\|
*	Add lemmas about always_invert_Some and bind	Jason Gross	2018-02-17
\|
*	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
\|