Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Don't rely on autogenerated names | 2017-06-05 | |
| | | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). | ||
* | Add more context proper lemmas | 2017-05-16 | |
| | |||
* | Flip argument order on interp for easier Proper lemmas | 2017-05-16 | |
| | |||
* | Add context_equiv and prove some Proper lemmas | 2017-05-16 | |
| | |||
* | Flip order of extendb, lookup arguments | 2017-05-16 | |
| | | | | This allows better Proper lemmas | ||
* | Remove useless argument | 2017-05-16 | |
| | |||
* | Add Interp_compile | 2017-05-16 | |
| | |||
* | Slightly better type for Interp_InterpToPHOAS | 2017-05-16 | |
| | |||
* | Add Named.ExprInversion | 2017-05-15 | |
| | |||
* | Add Wf_from_unit | 2017-05-15 | |
| | | | | | This one is much easier to compute with, and it means we can get rid of a lot of pesky Named.wff proofs. | ||
* | Add src/Compilers/Z/Named/DeadCodeEliminationInterp.v | 2017-05-15 | |
| | |||
* | Add DeadCodeEliminationInterp | 2017-05-15 | |
| | |||
* | Add a stronger lemma to registerassigninterp | 2017-05-15 | |
| | |||
* | Add GetNames | 2017-05-14 | |
| | |||
* | Add Named.default_names_for | 2017-05-14 | |
| | |||
* | Add Named.CountLets | 2017-05-14 | |
| | |||
* | Split off EliminateDeadCode | 2017-05-14 | |
| | |||
* | Fix some scoping | 2017-05-14 | |
| | |||
* | Allow specifying type in nlet | 2017-05-14 | |
| | |||
* | Support destructuring dlet and slet | 2017-05-13 | |
| | | | | | The current way to support it is a kludge around the fact that `x binder` only works for recursive notations | ||
* | Prove interp correctness of register reassign | 2017-04-13 | |
| | |||
* | Add Named.Syntax.Interp | 2017-04-13 | |
| | |||
* | Add lookupb_remove | 2017-04-13 | |
| | |||
* | Add lookupb_removeb_same | 2017-04-13 | |
| | |||
* | Add lookupb_remove_not_in | 2017-04-13 | |
| | |||
* | Add ContextOnOk | 2017-04-13 | |
| | |||
* | Remove dead code in comments | 2017-04-13 | |
| | |||
* | Reorder parameters for ease of partial instantiation, add symbolic_expr_dec | 2017-04-10 | |
| | |||
* | Add lookupb_extendb_full | 2017-04-10 | |
| | |||
* | Relax extendb, and prove a property about length | 2017-04-10 | |
| | |||
* | Add AListContext, WeakListContext | 2017-04-10 | |
| | |||
* | Split off Compilers.Named.Context | 2017-04-10 | |
| | |||
* | rename-everything | 2017-04-06 | |