Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Add type.related_hetero | 2018-07-30 | |
* | Generalize type.eqv a bit | 2018-07-30 | |
* | Integrate Wf and Interp proofs | 2018-07-30 | |
* | More proofs about wf / interp | 2018-07-27 | |
* | Add invert_nil, invert_cons | 2018-07-27 | |
* | Set arguments of ident.{gen_,}interp | 2018-07-27 | |
* | Put == in type_scope, so that we don't need to go around opening etype_scope | 2018-07-26 | |
* | Add type.eqv for interp equivalence | 2018-07-26 | |
* | Add invert_LetIn | 2018-07-25 | |
* | Montgomery reduction in new pipeline | 2018-07-21 | |
* | Support reification of firstn, skipn | 2018-07-18 | |
* | Allow reification of nat_rect (fun _ => _ -> _) | 2018-07-15 | |
* | Correctly reify match on prod | 2018-07-03 | |
* | WIP | 2018-07-03 | |
* | Make all parameters implicit | 2018-07-02 | |
* | Remove useless Requires | 2018-06-28 | |
* | New pipeline, split among files | 2018-06-17 |