| Commit message (Expand) | Author | Age |
* | 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 |
* | Add ZUtil.Sorting | Jason Gross | 2018-06-29 |
* | Revert "Add more schemes for prod" | Jason Gross | 2018-06-28 |
* | Add more schemes for prod | Jason Gross | 2018-06-28 |
* | Try out stronger land, lor bounds | Jason Gross | 2018-06-27 |
* | Add is_tighter_than_bool lemmas | Jason Gross | 2018-06-27 |
* | Add lnot mod pull/push lemmas | Jason Gross | 2018-06-27 |
* | Add missing Z.lnot_0 hints | Jason Gross | 2018-06-27 |
* | Add more Z const hints | Jason Gross | 2018-06-27 |
* | Remove lneg in favor of lnot_modulo (lneg was wrong) | Jason Gross | 2018-06-27 |
* | Add some Z.land, Z.lor hints | Jason Gross | 2018-06-27 |
* | Add a couple of zrange lemmas | Jason Gross | 2018-06-26 |