aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InterpProofs.v
Commit message (Expand)AuthorAge
* Add reflective_interp rewrite dbGravatar Jason Gross2017-04-02
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Add interpf_LetInGravatar Jason Gross2016-11-17
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Work around bug #5149 in 8.6 (broken subst, evars)Gravatar Jason Gross2016-10-18
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Better implicits for interpf, pointwise-lifting of rels over interp_type_genGravatar Jason Gross2016-09-05
* More 8.4 fixesGravatar Jason Gross2016-09-05
* PHOAS syntaxGravatar Jason Gross2016-09-05