aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z/Syntax.v
Commit message (Expand)AuthorAge
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Add BoundsInterpretationsGravatar Jason Gross2017-02-23
* Reorder Reflection.Z.SyntaxGravatar Jason Gross2017-02-02
* Split up Reflection/Z/Syntax and make it smallerGravatar Jason Gross2017-02-02
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Split out Reflection.Equality, change Tflat implicit argumentGravatar Jason Gross2017-01-19
* Remove an admitGravatar Jason Gross2016-11-17
* Make [neg] a unary operation in reflectionGravatar Jason Gross2016-11-11
* Remove special code for reified conditional subGravatar Jason Gross2016-11-11
* Fixes for Coq 8.4Gravatar Jason Gross2016-11-06
* Preliminary support: conditional sub as primitiveGravatar Jason Gross2016-11-06
* Switch to a faster way of proving wfGravatar Jason Gross2016-10-30
* Minor reflective changesGravatar Jason Gross2016-10-30
* Add interp_type_gen_rel_pointwise2, *_gen => *Gravatar Jason Gross2016-10-28
* Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 13:55:56 +0000