aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z
Commit message (Expand)AuthorAge
* 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
* Fix an infinite loopGravatar Jason Gross2016-10-29
* 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
* Add Inline importGravatar Jason Gross2016-10-27
* Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 09:54:53 +0000