aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/TestCase.v
Commit message (Expand)AuthorAge
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Switch to a faster way of proving wfGravatar Jason Gross2016-10-30
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
* Fix for Coq < 8.6Gravatar Jason Gross2016-09-22
* Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
* Make the example a function for reificationGravatar Jason Gross2016-09-18
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Fixes for Coq 8.4Gravatar Jason Gross2016-09-07
* Remove the need for coercions in well-typing of ReifyGravatar 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
* Better implicit arguments for wf typesGravatar Jason Gross2016-09-05
* Add comments to WfReflective, handle ExprGravatar Jason Gross2016-09-05
* Remove ReifyDirectGravatar Jason Gross2016-09-05
* A helper lemma for [Wf]Gravatar Jason Gross2016-09-05
* PHOAS syntaxGravatar Jason Gross2016-09-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 04:52:54 +0000