aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z
Commit message (Expand)AuthorAge
* Minor refactoring of related_Z_opGravatar Jason Gross2016-11-07
* Finish related_bounds_t_map1_tuple2Gravatar 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
* Some progress on Relations admitsGravatar Adam Chlipala2016-11-07
* 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
* Fixes for Coq 8.4Gravatar Jason Gross2016-11-06
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* More partial proofsGravatar Jason Gross2016-11-06
* Prove inversion principles for bounded wordsGravatar Jason Gross2016-11-06
* Add related_word64_boundsi'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
* More judgmental unification in Z.InterpretationsGravatar Jason Gross2016-11-05
* Add proj_option2 to Z.InterpretationsGravatar Jason Gross2016-11-05
* Fix implicits of Let for 8.4Gravatar Jason Gross2016-11-04
* Shove Z.Interpretations into closer alignmentGravatar Jason Gross2016-11-03
* Rearrangement to different judgmentally equal termsGravatar Jason Gross2016-11-03
* Add more projections in interpretationsGravatar Jason Gross2016-11-03
* Fix 8.4 build partiallyGravatar Jason Gross2016-11-03
* Add more interpretation thingsGravatar Jason Gross2016-11-03
* More relatednessGravatar Jason Gross2016-11-03
* Add more relatedness thingsGravatar Jason Gross2016-11-03
* Work around divergence of unification in Coq 8.5{,pl1}Gravatar Jason Gross2016-11-02
* Write code to lift option types over tuplesGravatar Jason Gross2016-11-02
* Fix bounds on neg in interpretationsGravatar Jason Gross2016-11-02
* Prove fe25519WToZ_ZToW, rename FooToBarToFoo to BarToFoo_FooToBarGravatar Jason Gross2016-11-01
* Fix and prove bounds for cmovne, cmovle; note a problem with the neg boundGravatar Jason Gross2016-11-01
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Safer definitions of shl, shrGravatar Jason Gross2016-10-31
* Fix a typo making word calculations wrongGravatar Jason Gross2016-10-31
* Also construct relatedness proofs in reifiedGravatar Jason Gross2016-10-30
* Fix tactic notation scope in the 8.5 buildGravatar Jason Gross2016-10-30
* Remove an [About]Gravatar Jason Gross2016-10-30
* Renaming in Reflection/Z/Interpretations.v, admitted rel lemmasGravatar Jason Gross2016-10-30
* Switch to a faster way of proving wfGravatar Jason Gross2016-10-30
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
* Revert "Premature optimization of [Reify_rhs]"Gravatar Jason Gross2016-10-30
* Premature optimization of [Reify_rhs]Gravatar Jason Gross2016-10-30
* Make Z Reification handle correctness proofsGravatar Jason Gross2016-10-30
* Generalize InputSyntax.Compile_correctGravatar Jason Gross2016-10-30
* Minor reflective changesGravatar Jason Gross2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:53:28 +0000