aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* 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
* Fix buildGravatar Jason Gross2016-11-03
* More relatednessGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Make apply things go through interp_flat_typeGravatar Jason Gross2016-11-03
* Versions of [Apply] that guarantee flat thingsGravatar 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
* Work around bug #5175 in 8.6Gravatar Jason Gross2016-11-01
* Add version of [Apply] for [Interp] thingsGravatar Jason Gross2016-10-31
* Add Reflection.ApplicationGravatar Jason Gross2016-10-31
* Add SmartVarMap_heteroGravatar Jason Gross2016-10-31
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Implicits for SmartVarMapTGravatar Jason Gross2016-10-31
* Add SmartVarMapTGravatar Jason Gross2016-10-31
* Safer definitions of shl, shrGravatar Jason Gross2016-10-31
* Fix a typo making word calculations wrongGravatar Jason Gross2016-10-31
* Interpret syntax with Let_InGravatar 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
* Generalize interp_flat_type_rel_pointwise2 a bitGravatar Jason Gross2016-10-30
* Minor changes to GF25519 reflectiveGravatar Jason Gross2016-10-30
* Handle 4 arguments in ReifyGravatar 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
* Fix slowness in [Defined] after [Reify_rhs]Gravatar Jason Gross2016-10-30
* Make Z Reification handle correctness proofsGravatar Jason Gross2016-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 11:21:42 +0000