aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z/Interpretations.v
Commit message (Expand)AuthorAge
* Finish related_bounds_t_map1_tuple2Gravatar Jason Gross2016-11-07
* Refactor various reflective thingsGravatar Jason Gross2016-11-06
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Prove inversion principles for bounded wordsGravatar Jason Gross2016-11-06
* 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
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Some work on proofs in src/Reflection/Z/Interpretations.vGravatar Jason Gross2016-10-27
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:18:36 +0000