aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Reify.v
Commit message (Expand)AuthorAge
* More robust reifierGravatar Jason Gross2017-03-29
* Add debug output for success in reifyfGravatar Jason Gross2017-03-22
* Switch to fully uncurried form for reflectionGravatar Jason Gross2017-03-01
* Various minor reflection fixupsGravatar Jason Gross2017-01-27
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Add support for dependent reificationGravatar Jason Gross2016-11-06
* Add some interpretations things, speed up proofs in Ed25519Gravatar Jason Gross2016-10-31
* Handle 4 arguments in ReifyGravatar Jason Gross2016-10-30
* Revert "Premature optimization of [Reify_rhs]"Gravatar Jason Gross2016-10-30
* Premature optimization of [Reify_rhs]Gravatar Jason Gross2016-10-30
* Fix slowness in [Defined] after [Reify_rhs]Gravatar Jason Gross2016-10-30
* Make Z Reification handle correctness proofsGravatar Jason Gross2016-10-30
* Factor out prove_compile_correctGravatar Jason Gross2016-10-30
* Adjust arguments to InputSyntax.CompileGravatar Jason Gross2016-10-30
* Generalize Reify a bitGravatar Jason Gross2016-10-30
* Generalize InputSyntax.Compile_correctGravatar Jason Gross2016-10-30
* Factor Reify_rhs so that it's more reusableGravatar Jason Gross2016-10-30
* Handle Let_In in reificationGravatar Jason Gross2016-10-29
* Fix type reificationGravatar Jason Gross2016-10-29
* Finer grained type reificationGravatar 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
* Remove the need for coercions in well-typing of ReifyGravatar Jason Gross2016-09-07
* Add fastpath to reify, add coercionsGravatar Jason Gross2016-09-07
* Key on the head of the operation in reificationGravatar Jason Gross2016-09-07
* Better implicits for InterpGravatar Jason Gross2016-09-05
* Remove ReifyDirectGravatar Jason Gross2016-09-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 13:47:12 +0000