aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/LinearizeInterp.v
Commit message (Expand)AuthorAge
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05