aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/WfProofs.v
Commit message (Expand)AuthorAge
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Move things to ExprInversionGravatar Jason Gross2016-12-03
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
* Add more WfProofsGravatar Jason Gross2016-10-29
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Reorder WfProofs argumentsGravatar Jason Gross2016-09-05
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05