aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Minor refactoring of related_Z_opGravatar Jason Gross2016-11-07
* Finish related_bounds_t_map1_tuple2Gravatar Jason Gross2016-11-07
* Add push_lift_optionGravatar Jason Gross2016-11-07
* More progress on related_bounds_t_map1_tuple2Gravatar Jason Gross2016-11-07
* More progress on t_map1_tuple2 lemmasGravatar Jason Gross2016-11-07
* Add flat_interp_tuple_untuple'Gravatar Jason Gross2016-11-07
* Add flat_interp_untuple'_tupleGravatar Jason Gross2016-11-07
* Add map_is_mapt'Gravatar Jason Gross2016-11-07
* Add IffT, some Proper prod lemmasGravatar Jason Gross2016-11-07
* Add Proper prod instanceGravatar Jason Gross2016-11-07
* Add convoy_destructGravatar Jason Gross2016-11-07
* Add tuple hd and tlGravatar Jason Gross2016-11-07
* Merge branch 'master' of ssh://github.com/mit-plv/fiat-cryptoGravatar Adam Chlipala2016-11-07
|\
* | Some progress on Relations admitsGravatar Adam Chlipala2016-11-07
| * automate MxDHRepChange.Proper_loopiter introsGravatar Andres Erbsen2016-11-07
|/
* implement X25519Gravatar Andres Erbsen2016-11-06
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* More reorg in Reflection/Z/Interpretations/Relations.vGravatar Jason Gross2016-11-06
* Do some of the related_Z_op proofsGravatar Jason Gross2016-11-06
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
* Add more admitted tuple lemmasGravatar Jason Gross2016-11-06
* Add Tuple.map_map2 (admitted)Gravatar Jason Gross2016-11-06
* Add HList lemmaGravatar Jason Gross2016-11-06
* Add admitted lemma about tuple map, add hlist lemGravatar Jason Gross2016-11-06
* Add Tuple lift pushGravatar Jason Gross2016-11-06
* Connect [is_bounded] to [bounded_by]Gravatar Jason Gross2016-11-06
* Fixes for Coq 8.4Gravatar Jason Gross2016-11-06
* The fix in 8.4 broke 8.5/8.6, so we fix thatGravatar Jason Gross2016-11-06
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Add syntactic tuplesGravatar Jason Gross2016-11-06
* Add functions for [tuple (option _) _]Gravatar Jason Gross2016-11-06
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* Work around broken evars in 8.4Gravatar Jason Gross2016-11-06
* More partial proofsGravatar Jason Gross2016-11-06
* Prove inversion principles for bounded wordsGravatar Jason Gross2016-11-06
* Plug in boundedness proofsGravatar Jason Gross2016-11-05
* Add better bounded lemmas to reified thingsGravatar Jason Gross2016-11-05
* Add eta-expansion in GF25519BoundedCommon.vGravatar Jason Gross2016-11-05
* Add proofs about boundedness to GF25519Reflective/Common.vGravatar Jason Gross2016-11-05
* Add unfold_is_boundedGravatar Jason Gross2016-11-05
* Add related_word64_boundsi'Gravatar Jason Gross2016-11-05
* Add code for overflow check (disabled bc freeze)Gravatar Jason Gross2016-11-05
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
* Fix implicit argumentsGravatar Jason Gross2016-11-05
* Remove pasted code that shouldn't've been in a fileGravatar Jason Gross2016-11-05
* Add proj1_from_option2Gravatar Jason Gross2016-11-05
* Fix implicitsGravatar Jason Gross2016-11-05
* Fix a proof broken by previous commitGravatar Jason Gross2016-11-05
* Another projection functionGravatar Jason Gross2016-11-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:10:11 +0000