fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix a name clash	Jason Gross	2017-03-14
\|
*	Add split_{m,o,}names_firstn_skipn and co.	Jason Gross	2017-03-14
\|
*	Add firstn_skipn	Jason Gross	2017-03-14
\|
*	Add split_prod	Jason Gross	2017-03-14
\|
*	Add NameUtilProperties	Jason Gross	2017-03-14
\|
*	Add skipn_skipn	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOASInterp	Jason Gross	2017-03-14
\|
*	Add Wf_InterpToPHOAS	Jason Gross	2017-03-14
\|
*	Remove useless hyps	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOAS	Jason Gross	2017-03-14
\|
*	Move find_if_eq to Decidable.v, use Decidable in Named	Jason Gross	2017-03-14
\|
*	Add ContextProperties	Jason Gross	2017-03-14
\|
*	Remove useless imports	Jason Gross	2017-03-14
\|
*	Move ContextOk to ContextDefinitions	Jason Gross	2017-03-14
\|
*	Add lemma about wff and interpf of Named	Jason Gross	2017-03-14
\|
*	Add faster versions of destruct_head_*	Jason Gross	2017-03-14
\| \| \| \|	Sometimes, it's a performance bottleneck
*	Fix more unfolding	Jason Gross	2017-03-10
\|
*	Fix more unfolding that shouldn't happen	Jason Gross	2017-03-10
\|
*	Make sure interp_flat_type isn't unfolded in SmartMap	Jason Gross	2017-03-10
\|
*	Add better SmartFlatTypeMapInterp2	Jason Gross	2017-03-08
\|
*	Remove interp_genf from Named/Syntax	Jason Gross	2017-03-08
\|
*	Remove stuff from Reflection/Named/Syntax	Jason Gross	2017-03-08
\|
*	Add FMapContext, PositiveContext	Jason Gross	2017-03-08
\| \| \| \| \|	Also copy some definitions from Syntax out of it, in prep for removing them
*	Fixes #127	jadep	2017-03-06
\|
*	Remove assert_preconditions; prove ring-ness of basesystem operations for ↵	jadep	2017-03-04
\| \| \| \|	base 2^25.5
*	Separated out specific test cases for new base system	jadep	2017-03-04
\|
*	Fixed admit left from fsatz port	jadep	2017-03-02
\|
*	make 8.5 happy	Andres Erbsen	2017-03-02
\|
*	fixup NewBasesystem	Andres Erbsen	2017-03-02
\|
*	remove dangling file that gives a warning	Andres Erbsen	2017-03-02
\|
*	remove undeclared lines from Ed25519Extraction.v	Andres Erbsen	2017-03-02
\|
*	move large non-building chunks of Ed25519.v	Andres Erbsen	2017-03-02
\|
*	deleted src/Specific/GF25519ExtendedAddCoordinates.v	Andres Erbsen	2017-03-02
\|
*	fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v	Andres Erbsen	2017-03-02
\|
*	remove PointEncoding	Andres Erbsen	2017-03-02
\|
*	CompleteEdwardsCurveTheorems: point compression	Andres Erbsen	2017-03-02
\|
*	PrimeFieldTheorems: inv for isomorphic fields	Andres Erbsen	2017-03-02
\|
*	use [positive] for [F] modulus, char_ge_C instead of char_gt_C	Andres Erbsen	2017-03-02
\|
*	rewrite ExtendedCoordinates, fix Ed25519	Andres Erbsen	2017-03-02
\|
*	edwards curves over isomorphic fields	Andres Erbsen	2017-03-02
\|
*	src/Tactics/Algebra_syntax/Nsatz.v: power 1 only	Andres Erbsen	2017-03-02
\|
*	WIP	Andres Erbsen	2017-03-02
\|
*	address some code review comments	Andres Erbsen	2017-03-02
\|
*	Weierstrass curve is a group	Andres Erbsen	2017-03-02
\|
*	Attempt Weierstrass associativity again, good progress.	Andres Erbsen	2017-03-02
\|
*	change weierstrass spec, prove most cases of associativity	Andres Erbsen	2017-03-02
\|
*	split the algebra library; use fsatz more	Andres Erbsen	2017-03-02
\|
*	fsatz, nsatz_solve_nonzero	Andres Erbsen	2017-03-02
\|
*	use field_nsatz in CompleteEdwardsCurve.Pre	Andres Erbsen	2017-03-02
\|
*	field_nsatz	Andres Erbsen	2017-03-02
\|