| Commit message (Expand) | Author | Age |
|---|
| * | Backwards compatible fix for some issues from https://github.com/coq/coq/pull... |  Jason Gross | 2018-08-04 |
| * | Add wf for DefaultValue |  Jason Gross | 2018-08-03 |
| * | Add wf_splice_list, wf_splice_list_no_order | Jason Gross | 2018-08-03 |
| * | Fix typo in previous commit | Jason Gross | 2018-08-03 |
| * | Add eq_ident_Decidable | Jason Gross | 2018-08-03 |
| * | Add reflect_list_cps_id | Jason Gross | 2018-08-03 |
| * | Better rewrite_type_transport_correct | Jason Gross | 2018-08-02 |
| * | Adjust GENERATEDIdentifiersWithoutTypesProofs.v, add eta_ident_cps_correct | Jason Gross | 2018-08-02 |
| * | Add GENERATEDIdentifiersWithoutTypesProofs.v | Jason Gross | 2018-08-02 |
| * | Also generate decidable equality for pattern.ident | Jason Gross | 2018-08-02 |
| * | Make wf_safe_t a bit stronger | Jason Gross | 2018-08-02 |
| * | Make ERROR_BAD_REWRITE_RULE Opaque, not Qed'ed | Jason Gross | 2018-08-02 |
| * | Generalize option_eq to support heterogenous relations | Jason Gross | 2018-08-02 |
| * | Add nth_error_combine | Jason Gross | 2018-08-01 |
| * | More precise wf_Proper_list_impl | Jason Gross | 2018-07-31 |
| * | Comment out wf_splice_list | Jason Gross | 2018-07-31 |
| * | Add wf_Proper_list, wf_splice_list | Jason Gross | 2018-07-31 |
| * | Add type.related_hetero | Jason Gross | 2018-07-30 |
| * | Fix some issues in previous commit | Jason Gross | 2018-07-30 |
| * | Add nat_rect_Proper_nondep_gen | Jason Gross | 2018-07-30 |
| * | Allow proving force ∘ thunk = id extensionally | Jason Gross | 2018-07-30 |
| * | Add UnderLets.wf_Proper_list | Jason Gross | 2018-07-30 |
| * | Add wf_splice | Jason Gross | 2018-07-30 |
| * | Generalize type.eqv a bit | Jason Gross | 2018-07-30 |
| * | Some WIP on Rewiter correctness | Jason Gross | 2018-07-30 |
| * | Integrate Wf and Interp proofs | Jason Gross | 2018-07-30 |
| * | Add wf and interp proofs for LetBindReturn | Jason Gross | 2018-07-27 |
| * | More proofs about wf / interp | Jason Gross | 2018-07-27 |
| * | Add wf about reify/reflect list | Jason Gross | 2018-07-27 |
| * | Stronger inversion | Jason Gross | 2018-07-27 |
| * | Add invert_nil, invert_cons | Jason Gross | 2018-07-27 |
| * | Set arguments of ident.{gen_,}interp | Jason Gross | 2018-07-27 |
| * | Move rewrites to the correct tactic | Jason Gross | 2018-07-26 |
| * | Shuffle transport lemmas around, add more inversion | Jason Gross | 2018-07-26 |
| * | Add Wf proofs about MiscCompilerPasses | Jason Gross | 2018-07-26 |
| * | Move the associator pass to the rewriter | Jason Gross | 2018-07-26 |
| * | Improve wf tactics | Jason Gross | 2018-07-26 |
| * | Minor improvements to wf framework | Jason Gross | 2018-07-26 |
| * | Move some tactics to their proper place | Jason Gross | 2018-07-26 |
| * | Add Wf lemmas about SubstVar | Jason Gross | 2018-07-26 |
| * | Put == in type_scope, so that we don't need to go around opening etype_scope | Jason Gross | 2018-07-26 |
| * | Add basic wf proofs | Jason Gross | 2018-07-26 |
| * | Actually improve expr.invert_one | Jason Gross | 2018-07-26 |
| * | Try again to fix expr inversion | Jason Gross | 2018-07-26 |
| * | Improve expr.invert_one (hopefully) | Jason Gross | 2018-07-26 |
| * | Add more proper instances | Jason Gross | 2018-07-26 |
| * | Add type.eqv for interp equivalence | Jason Gross | 2018-07-26 |
| * | Add some inversion lemmas and tactics | Jason Gross | 2018-07-25 |
| * | Add invert_LetIn | Jason Gross | 2018-07-25 |
| * | Reserve ==, ===, ~= | Jason Gross | 2018-07-25 |
Jason Gross
Jason Gross