| Commit message (Expand) | Author | Age |
* | Add do_with_exactly_one_hyp | Jason Gross | 2018-08-29 |
* | Minor improvements to various ZUtil things; bounds | Jason Gross | 2018-08-25 |
* | Minor rshi tweaks | Jason Gross | 2018-08-24 |
* | Add some cc_m morphisms | Jason Gross | 2018-08-24 |
* | Add Z.rshi_correct_full | Jason Gross | 2018-08-24 |
* | Add Z.cc_m_eq_full | Jason Gross | 2018-08-24 |
* | Add some basic ZRange lemmas | Jason Gross | 2018-08-24 |
* | Add ZRange.union_comm | Jason Gross | 2018-08-24 |
* | Add a few more zsimplify_const lemmas about shift | Jason Gross | 2018-08-24 |
* | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | Jason Gross | 2018-08-23 |
* | Fix bounds on n_corners_and_zero | Jason Gross | 2018-08-16 |
* | Prove monotonicity properties about zrange | Jason Gross | 2018-08-15 |
* | Add more zutil morphisms | Jason Gross | 2018-08-13 |
* | Fix some bounds analysis | Jason Gross | 2018-08-13 |
* | Add some Z.le Proper hints to zarith | Jason Gross | 2018-08-13 |
* | Fix previous commit | Jason Gross | 2018-08-13 |
* | Move a lemma | Jason Gross | 2018-08-13 |
* | Add the file proving split_bounds correct | Jason Gross | 2018-08-13 |
* | Fix split_bounds, prove it correct | Jason Gross | 2018-08-13 |
* | Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool... | Jason Gross | 2018-08-13 |
* | Add some util lemmas | Jason Gross | 2018-08-13 |
* | Add ListUtil.map_nth_default_seq | Jason Gross | 2018-08-10 |
* | Make Prod.eta_expand also work in the context | Jason Gross | 2018-08-10 |
* | Add ListUtil.{combine_repeat,combine_rev_rev_samelength} | Jason Gross | 2018-08-09 |
* | Improve the power of split_andb | Jason Gross | 2018-08-09 |
* | Reserve 'n notation in Notations.v | Jason Gross | 2018-08-08 |
* | Add related_iff_app_curried | Jason Gross | 2018-08-06 |
* | Generalize option_eq to support heterogenous relations | Jason Gross | 2018-08-02 |
* | Add nth_error_combine | Jason Gross | 2018-08-01 |
* | Fix some issues in previous commit | Jason Gross | 2018-07-30 |
* | Add nat_rect_Proper_nondep_gen | Jason Gross | 2018-07-30 |
* | Add more proper instances | Jason Gross | 2018-07-26 |
* | Reserve ==, ===, ~= | Jason Gross | 2018-07-25 |
* | Add option sequencing/return | Jason Gross | 2018-07-25 |
* | Reserve ;;;, fix level of prefix # to not clash with infix # | Jason Gross | 2018-07-25 |
* | Add ListUtil.{take,drop}_while | Jason Gross | 2018-07-24 |
* | Make Z.modinv run on wf proofs | Jason Gross | 2018-07-18 |
* | Handle Z.pow in push_Zmod tactic | Jason Gross | 2018-07-17 |
* | Handle Z.pow in {push,pull}_Zmod | Jason Gross | 2018-07-17 |
* | Add minor lemmas to util | Jason Gross | 2018-07-17 |
* | Make Z.div_mod_to_quot_rem stronger | Jason Gross | 2018-07-10 |
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
* | Fix an infinite loop in Z.peel_le | Jason Gross | 2018-07-06 |
* | Add ZUtil, list lemmas | Jason Gross | 2018-07-02 |
* | Fix a notation issue in previous commit | Jason Gross | 2018-07-02 |
* | Add more ListUtil proofs | Jason Gross | 2018-07-02 |
* | Add some list lemmas | Jason Gross | 2018-07-02 |
* | Make all parameters implicit | Jasper Hugunin | 2018-07-02 |
* | Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids | Jason Gross | 2018-07-01 |
* | Add useful list lemmas | Jason Gross | 2018-06-29 |