aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/InputSyntax.v
Commit message (Collapse)AuthorAge
* Add [f] to things that use [exprf] or [flat_type]Gravatar Jason Gross2016-10-31
|
* Interpret syntax with Let_InGravatar Jason Gross2016-10-31
|
* Adjust arguments to InputSyntax.CompileGravatar Jason Gross2016-10-30
|
* Generalize InputSyntax.Compile_correctGravatar Jason Gross2016-10-30
|
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
|
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
| | | | | We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q.
* Better implicits for interpf, pointwise-lifting of rels over interp_type_genGravatar Jason Gross2016-09-05
|
* Better implicits for InterpGravatar Jason Gross2016-09-05
|
* More 8.4 fixesGravatar Jason Gross2016-09-05
|
* PHOAS syntaxGravatar Jason Gross2016-09-05
We also have linearization of function application / lets, constant-inlining, and reification. This closes #58.