aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InlineWf.v
Commit message (Expand)AuthorAge
* 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