aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InlineWf.v
Commit message (Expand)AuthorAge
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Generalize InlineWfGravatar Jason Gross2017-02-13
* Add wf databaseGravatar Jason Gross2017-02-01
* Split off some bits of Reflection.SyntaxGravatar Jason Gross2017-01-26
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* More fine-grained util tactic filesGravatar Jason Gross2017-01-17
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* More 8.4 fixesGravatar Jason Gross2016-10-29
* Finish proof in src/Reflection/InlineWf.vGravatar Jason Gross2016-10-29
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16