| Commit message (Expand) | Author | Age |
|---|
| * | Move le_{add,sub}_1_* to ZUtil.Le |  Jason Gross | 2018-12-25 |
| * | from_montgomery{_ => }mod, for consistency with other naming | Jason Gross | 2018-12-24 |
| * | Add correctness in arithmetic for mulx, addcarryx, subborrowx | Jason Gross | 2018-12-21 |
| * | Add has_body tactic | Jason Gross | 2018-12-21 |
| * | Add eval_freeze_to_bytesmod to push_eval | Jason Gross | 2018-12-21 |
| * | Add length_encode_no_reduce to distr_length | Jason Gross | 2018-12-21 |
| * | Add `Proof using` directives in Arithmetic | Jason Gross | 2018-12-21 |
| * | Fix a few minor things in Arithmetic | Jason Gross | 2018-12-21 |
| * | remove unneeded lemma and do some micro-performance-optimization at one stick... |  jadep | 2018-12-21 |
| * | remove proof duplication | jadep | 2018-12-21 |
| * | fix hints and [Proof using] statements so that proofs go through | jadep | 2018-12-21 |
| * | prove [small_sub_then_maybe_add] | jadep | 2018-12-21 |
| * | prove [eval_sub_then_maybe_add] | jadep | 2018-12-21 |
| * | fix hints and [Proof using] statements so that proofs go through | jadep | 2018-12-21 |
| * | prove [small_conditional_sub] | jadep | 2018-12-21 |
| * | prove [eval_conditional_sub] | jadep | 2018-12-21 |
| * | move weight proofs up above Positional so they can be used to prove eval_drop... | jadep | 2018-12-21 |
| * | modify a proof because in 8.7 [auto] doesn't solve the goal | jadep | 2018-12-21 |
| * | prove admit | jadep | 2018-12-21 |
| * | prove admit | jadep | 2018-12-21 |
| * | Add Wf_reify | Jason Gross | 2018-12-20 |
| * | Add Wf_APP, Interp_reify | Jason Gross | 2018-12-20 |
| * | Remove glue admits in Toplevel1 | Jason Gross | 2018-12-20 |
| * | Add uweight_partition_unique, move weight_1 to uweight_1, add Positional.eval... | Jason Gross | 2018-12-20 |
| * | Finish rewriter proofs modulo funext | Jason Gross | 2018-12-19 |
| * | Add eq_subst_types_pattern_collect_vars_empty_iff | Jason Gross | 2018-12-18 |
| * | Add rawexpr_types_ok | Jason Gross | 2018-12-14 |
| * | Fix an issue with setoid_rewrite being weaker before 8.9 | Jason Gross | 2018-12-14 |
| * | Add reify_and_let_binds_base_interp_related | Jason Gross | 2018-12-14 |
| * | add interp_related_gen_of_wf | Jason Gross | 2018-12-12 |
| * | Remove useless assumptions | Jason Gross | 2018-12-12 |
| * | Generalize expr.interp_related | Jason Gross | 2018-12-12 |
| * | Move fancy rewrites after bounds analysis | Jason Gross | 2018-12-12 |
| * | Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565d | Jason Gross | 2018-12-12 |
| * | Add type.eq_subst_types_pattern_collect_vars | Jason Gross | 2018-12-12 |
| * | Make unify_pattern' a bit stricter | Jason Gross | 2018-12-12 |
| * | Add projT1_app_with_unification_resultT | Jason Gross | 2018-12-12 |
| * | Add rawexpr_interp_related_Proper_rawexpr_equiv_rew_gen | Jason Gross | 2018-12-12 |
| * | Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_m | Jason Gross | 2018-12-11 |
| * | Add ZRange.is_bounded_by_bool_normalize_constant | Jason Gross | 2018-12-11 |
| * | Add ZRange.normalize_constant | Jason Gross | 2018-12-11 |
| * | Add ZRange.is_bounded_by_bool_constant | Jason Gross | 2018-12-11 |
| * | Add ZRange.OperationBounds | Jason Gross | 2018-12-11 |
| * | remove pattern.ident.type_vars | Jason Gross | 2018-12-11 |
| * | Use Fixpoint, not list_rect, for {app,lam}_forall_vars | Jason Gross | 2018-12-11 |
| * | Add In_elements_mem_iff | Jason Gross | 2018-12-11 |
| * | Add eqv_iff_eq_of_funext | Jason Gross | 2018-12-11 |
| * | Prove pattern.ident.type_vars_enough | Jason Gross | 2018-12-08 |
| * | Add value_of_rawexpr_interp_related | Jason Gross | 2018-12-07 |
| * | Switch to a more precise version of interp_related for rewrites | Jason Gross | 2018-12-07 |
Jason Gross
jadep