aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* 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
* 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
* PHOAS notation fixupsGravatar Jason Gross2016-10-27
* Make it easier to export only phoas notationsGravatar Jason Gross2016-10-27
* add wf, not only rel_wf, to MapInterpWfGravatar Jason Gross2016-10-27
* Add WfRelReflectiveGravatar Jason Gross2016-10-27
* Factor WfReflective through WfReflectiveGenGravatar Jason Gross2016-10-27
* Implicits for reflect_wfTGravatar Jason Gross2016-10-27
* Add WfReflectiveGenGravatar Jason Gross2016-10-27
* Move interp_flat_type_gen_rel_pointwise2 to SyntaxGravatar Jason Gross2016-10-27
* Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
* Add arguments to mapf_interp_flat_type_genGravatar Jason Gross2016-10-27
* Add implicits to interp_flat_type_gen_rel_pointwise2Gravatar Jason Gross2016-10-27
* Change the argument implicits on rel_wffGravatar Jason Gross2016-10-27
* Work around bug #5149 in 8.6 (broken subst, evars)Gravatar Jason Gross2016-10-18
* Add a variant of [map] on reflective things that changes the interp functionGravatar Jason Gross2016-10-07
* Fix a spelling typoGravatar Jason Gross2016-10-02
* Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
* Fix for Coq < 8.6Gravatar Jason Gross2016-09-22
* Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
* Add dead code eliminationGravatar Jason Gross2016-09-22
* Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
* Generalize count_letsGravatar Jason Gross2016-09-21
* Deduplicate codeGravatar Jason Gross2016-09-21
* Add some util files for reflective let bindingsGravatar Jason Gross2016-09-21
* Generalize InlineConstGravatar Jason Gross2016-09-20
* Make the example a function for reificationGravatar Jason Gross2016-09-18
* Better arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Arguments for SmartVarMapGravatar Jason Gross2016-09-18
* Generalize SmartVarVarGravatar Jason Gross2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Generalize InlineConstGravatar Jason Gross2016-09-16
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Add arguments for smartvalGravatar Jason Gross2016-09-16
* Fix a bad lineGravatar Jason Gross2016-09-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:23:26 +0000