aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* | Work around bug in 8.4Gravatar Jason Gross2016-11-08
* | Work around bug 5189 (broken [Hint Resolve ->])Gravatar Jason Gross2016-11-08
* | Add Z.lor_nonneg to zarithGravatar Jason Gross2016-11-08
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:29:57 +0000