aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* 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
* Factor out prove_compile_correctGravatar Jason Gross2016-10-30
* Adjust arguments to InputSyntax.CompileGravatar Jason Gross2016-10-30
* Generalize Reify a bitGravatar Jason Gross2016-10-30
* Generalize InputSyntax.Compile_correctGravatar Jason Gross2016-10-30
* Factor Reify_rhs so that it's more reusableGravatar Jason Gross2016-10-30
* Minor reflective changesGravatar Jason Gross2016-10-30
* Fix an infinite loopGravatar Jason Gross2016-10-29
* Handle Let_In in reificationGravatar Jason Gross2016-10-29
* Fix type reificationGravatar Jason Gross2016-10-29
* Finer grained type reificationGravatar Jason Gross2016-10-29
* More 8.4 fixesGravatar Jason Gross2016-10-29
* Fix for 8.4Gravatar Jason Gross2016-10-29
* Finish proof in src/Reflection/InlineWf.vGravatar Jason Gross2016-10-29
* Add more WfProofsGravatar Jason Gross2016-10-29
* Add InterpWfGravatar Jason Gross2016-10-28
* Add InterpWfRelGravatar Jason Gross2016-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-06 14:28:35 +0000