aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection
Commit message (Expand)AuthorAge
* 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
* Add SmartValGravatar Jason Gross2016-09-16
* Add generalized version of Wf parameterized on relGravatar Jason Gross2016-09-15
* Fixes for Coq 8.4Gravatar Jason Gross2016-09-07
* Remove the need for coercions in well-typing of ReifyGravatar Jason Gross2016-09-07
* Add fastpath to reify, add coercionsGravatar Jason Gross2016-09-07
* Key on the head of the operation in reificationGravatar Jason Gross2016-09-07
* Add Common Subexpression EliminationGravatar Jason Gross2016-09-06
* Fix for 8.4's type inferencer being brokenGravatar Jason Gross2016-09-06
* Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refoldingGravatar Jason Gross2016-09-06
* Fix for 8.6 (context (correctly) no longer defaults to type_scope)Gravatar Jason Gross2016-09-06
* Add interp_flat_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05
* Add instances for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interpf, pointwise-lifting of rels over interp_type_genGravatar Jason Gross2016-09-05
* Better implicits for interpfGravatar Jason Gross2016-09-05
* Better implicits for interpGravatar Jason Gross2016-09-05
* Better implicits for InterpGravatar Jason Gross2016-09-05
* Add LinearizeWfGravatar Jason Gross2016-09-05
* Reorder WfProofs argumentsGravatar Jason Gross2016-09-05
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05
* Better implicits for let_bind_constGravatar Jason Gross2016-09-05
* Better implicit arguments for under_letsfGravatar Jason Gross2016-09-05
* Better implicit arguments for linearizeGravatar Jason Gross2016-09-05
* Better implicit arguments for wf typesGravatar Jason Gross2016-09-05
* Update comment with Andres' suggestionGravatar Jason Gross2016-09-05
* More 8.4 fixesGravatar Jason Gross2016-09-05
* Add comments to WfReflective, handle ExprGravatar Jason Gross2016-09-05
* More 8.4 fixes (apparently rebinding [->] doesn't work)Gravatar Jason Gross2016-09-05
* Fix for 8.4 compatibilityGravatar Jason Gross2016-09-05
* Remove ReifyDirectGravatar Jason Gross2016-09-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:33:57 +0000