fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Rename Interp lemmas	Jason Gross	2017-02-21
\| \| \| \| \| \|	```bash $ git grep --name-only 'Interp_InlineCast\\|Interp_InlineConst\\|Interp_Linearize' \| xargs sed s'/Interp_/Interp/g' -i ```
*	Add non-exprf version of interpf_smart_unbound	Jason Gross	2017-02-16
\|
*	Add MapCastInterp	Jason Gross	2017-02-16
\|
*	Add InterpByIsoProofs	Jason Gross	2017-02-16
\|
*	Add more display logs	Jason Gross	2017-02-16
\|
*	Fix typo	Jason Gross	2017-02-16
\|
*	Add InterpByIso	Jason Gross	2017-02-16
\| \| \| \| \| \|	It's actually closer to interp_by_retraction... This lets you do [interp] on, e.g., products with fail-values (var * interp_base), as long as [var] is pointed.
*	Add more display logs	Jason Gross	2017-02-15
\|
*	Add some display logs	Jason Gross	2017-02-15
\|
*	Add some display logs	Jason Gross	2017-02-15
\|
*	./copy_bounds	Jason Gross	2017-02-15
\|
*	Add rudimentary Java and C notation files, display	Jason Gross	2017-02-15
\|
*	Remove useless comment	Jason Gross	2017-02-14
\|
*	Mostly finish Wf_Boundify	Jason Gross	2017-02-14
\|
*	Prove wff_bound_op	Jason Gross	2017-02-14
\|
*	Stub for wff_bound_op	Jason Gross	2017-02-14
\|
*	Add Wf_MapInterpCast to wf database	Jason Gross	2017-02-14
\|
*	A bit more progress on BoundByCastWf	Jason Gross	2017-02-14
\|
*	Add partially finished MapCastWf	Jason Gross	2017-02-14
\|
*	Add src/Reflection/BoundByCastWf.v	Jason Gross	2017-02-14
\|
*	Update assumptions in src/Reflection/SmartBoundWf.v	Jason Gross	2017-02-14
\|
*	Add SmartBoundWf	Jason Gross	2017-02-14
\|
*	Prove nicer version of wf_SmartAbs	Jason Gross	2017-02-13
\|
*	Add partially admitted lemma wf_SmartAbs	Jason Gross	2017-02-13
\|
*	More uniform naming	Jason Gross	2017-02-13
\|
*	Generalize EtaWf some (still one admit)	Jason Gross	2017-02-13
\|
*	Add InlineCastInterp.v	Jason Gross	2017-02-13
\|
*	Add InlineCastWf	Jason Gross	2017-02-13
\|
*	Better cleanup in type_inversion	Jason Gross	2017-02-13
\|
*	Better type_inversion	Jason Gross	2017-02-13
\| \| \| \|	Now we don't loop on [Unit = Unit] hypotheses, clearing them instead.
*	Split off inversion_wff for constr-only hyps	Jason Gross	2017-02-13
\|
*	Add inversion_type	Jason Gross	2017-02-13
\|
*	Generalize InlineWf	Jason Gross	2017-02-13
\|
*	Add SmartCast{Interp,Wf}	Jason Gross	2017-02-13
\|
*	Split up BoundByCast	Jason Gross	2017-02-13
\|
*	Generalize BoundByCast a bit	Jason Gross	2017-02-10
\| \| \| \|	The rules for handling \| / & vs >> are different; we can truncate early on \| / &, but not on >>
*	Add EtaInterp, EtaWf	Jason Gross	2017-02-10
\|
*	Use Eta in BoundByCast	Jason Gross	2017-02-10
\|
*	Add Reflection/Eta.v	Jason Gross	2017-02-10
\|
*	Fix a missing section close in ZToRing	Jason Gross	2017-02-10
\|
*	Add files for constant reflective notations	Jason Gross	2017-02-10
\|
*	Accidentally pushed wrong file in last commit; this is the correct one	jadep	2017-02-10
\|
*	Added ZToRing lemmas	jadep	2017-02-09
\|
*	Remove useless imports	Jason Gross	2017-02-08
\|
*	Factor things into BoundByCast.v	Jason Gross	2017-02-08
\|
*	Fix type inference bug in 8.6	Jason Gross	2017-02-08
\|
*	Simpler version of MapCast	Jason Gross	2017-02-08
\| \| \| \| \|	Unfortunately, more of the casting logic is in MultiSizeTest2, now. I plan to make it more generic soon.
*	Remove the let-in from SmartValf	Jason Gross	2017-02-07
\| \| \| \|	It messes with reduction elsewhere
*	Fix relation relb arguments	Jason Gross	2017-02-07
\|
*	Add things like interp_flat_type_rel_pointwise1_gen_Prop_iff_bool	Jason Gross	2017-02-07
\| \| \| \| \|	Because [simpl] unfolds things, so we want lemmas to rewrite with even after [simpl]