| Commit message (Expand) | Author | Age |
* | Add some minor reflect things | Jason Gross | 2019-03-04 |
* | Make [reflect] a typeclass and add a bunch of lemmas | Jason Gross | 2019-03-04 |
* | Add Option.{lift,map,combine}, List.Option.lift | Jason Gross | 2019-02-11 |
* | Add zrange_rect{,_Proper,_Proper_dep} | Jason Gross | 2019-02-02 |
* | Add option_beq_hetero | Jason Gross | 2019-02-02 |
* | Add remove_duplicates | Jason Gross | 2019-01-24 |
* | Define String.replace | Jason Gross | 2019-01-18 |
* | Remove ? notation | Jason Gross | 2019-01-17 |
* | Add some more basic ZRange lemmas | Jason Gross | 2019-01-15 |
* | Move StringMap into Strings/ | Jason Gross | 2019-01-15 |
* | Add StringMap | Jason Gross | 2019-01-15 |
* | Add String_as_OT | Jason Gross | 2019-01-15 |
* | Autocompute s and c in WBW Montgomery | Jason Gross | 2019-01-14 |
* | Move le_{add,sub}_1_* to ZUtil.Le | Jason Gross | 2018-12-25 |
* | Add has_body tactic | Jason Gross | 2018-12-21 |
* | prove [eval_conditional_sub] | jadep | 2018-12-21 |
* | 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 |
* | Add In_elements_mem_iff | Jason Gross | 2018-12-11 |
* | Add Forall2_update_nth | Jason Gross | 2018-12-06 |
* | Fix broken proofs | Jason Gross | 2018-12-04 |
* | Add more Forall2 lemmas | Jason Gross | 2018-12-04 |
* | Add more ListUtil Forall Lemmas | Jason Gross | 2018-12-04 |
* | Add some ListUtil lemmas about Forall2 | Jason Gross | 2018-12-04 |
* | Remove ListUtil.List.repeat | Jason Gross | 2018-12-04 |
* | Revert "Add inversion_clear tactics" | Jason Gross | 2018-12-04 |
* | Add inversion_clear tactics | Jason Gross | 2018-12-04 |
* | Global Set Fast Name Printing | Jason Gross | 2018-11-27 |
* | Add related_sigT_by_eq proper lemmas | Jason Gross | 2018-11-19 |
* | Add more reserved notations | Jason Gross | 2018-11-19 |
* | Add related_sigT_by_eq | Jason Gross | 2018-11-16 |
* | Add map_repeat, map_const | Jason Gross | 2018-11-11 |
* | Add a variant of cps_id that pulls the continuation from the lhs | Jason Gross | 2018-11-08 |
* | Add some zrange lemmas | Jason Gross | 2018-11-01 |
* | Make pairs work in Z_cast2 | Jason Gross | 2018-11-01 |
* | Export ZRange operation notations | Jason Gross | 2018-11-01 |
* | Add zrange notations | Jason Gross | 2018-11-01 |
* | Add more reserved notations | Jason Gross | 2018-11-01 |
* | Add more zrange operations | Jason Gross | 2018-11-01 |
* | Tactic-in-term: ensuring same scope for all occurrences of a notation variable. | Hugo Herbelin | 2018-11-01 |
* | Add PositiveSet Facts | Jason Gross | 2018-10-29 |
* | Add eqlistA_eq_iff | Jason Gross | 2018-10-29 |
* | Add split_contravariant_or | Jason Gross | 2018-10-29 |
* | Add ex_eq_and tactic | Jason Gross | 2018-10-29 |
* | Add some lemmas about ex, and, eq | Jason Gross | 2018-10-29 |
* | Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tactics | Jason Gross | 2018-10-28 |
* | Fix a bug in ensure_complex_continuation | Jason Gross | 2018-10-28 |