| Commit message (Expand) | Author | Age |
* | Better Zmod manipulation | Jason Gross | 2016-08-03 |
* | Remove Bool.absorption_andb Bool.absorption_orb, not present in < 8.4pl5 | Jason Gross | 2016-08-03 |
* | Weaken some ZUtil assumptions | Jason Gross | 2016-08-03 |
* | More ZUtil | Jason Gross | 2016-08-03 |
* | More ZUtil | Jason Gross | 2016-08-03 |
* | Add ZUtil lemmas, and Util.Bool | Jason Gross | 2016-08-03 |
* | More zsimplify hints | Jason Gross | 2016-08-03 |
* | Add {push,pull}_Zdiv databases | Jason Gross | 2016-08-03 |
* | Add more ZUtil lemmas | Jason Gross | 2016-08-03 |
* | Mention Barrett reduction opt. in crypto-defects.md | Andres Erbsen | 2016-08-03 |
* | Note ref/sc25519.c:84 in crypto-defects.md | Andres Erbsen | 2016-08-03 |
* | Add some simplification lemmas to ZUtil | Jason Gross | 2016-08-02 |
* | Add pull_Zmod tactic | Jason Gross | 2016-08-01 |
* | Make Z.ltb_to_lt more powerful | Jason Gross | 2016-08-01 |
* | Add div lower/upper bounds to zarith hint db | Jason Gross | 2016-08-01 |
* | Better hint for div_to_inv_modulo | Jason Gross | 2016-08-01 |
* | Add a comment | Jason Gross | 2016-08-01 |
* | Better transparency of dec_eq_sig_hprop | Jason Gross | 2016-08-01 |
* | Add a lemma about removing division in modular arithmetic | Jason Gross | 2016-08-01 |
* | Add documentation: Equality, HProp, Isomorphism, Sigma (#41) | Jason Gross | 2016-08-01 |
* | Fixes for Coq 8.4 | Jason Gross | 2016-08-01 |
* | Add [0 mod _ = 0] to zsimplify db | Jason Gross | 2016-08-01 |
* | Add a tactic to eliminate hprop trivial proofs | Jason Gross | 2016-08-01 |
* | Remove useless hypotheses for [path_sigT_uncurried_iff] | Jason Gross | 2016-08-01 |
* | Add push_Zmod tactics | Jason Gross | 2016-07-29 |
* | Don't give equiv_modulo reflexive instance priority over eq | Jason Gross | 2016-07-29 |
* | Add more Z.modulo lemmas | Jason Gross | 2016-07-29 |
* | Add another ZUtil rewrite hint | Jason Gross | 2016-07-29 |
* | Add a ZUtil rewrite hint | Jason Gross | 2016-07-29 |
* | Add equiv_modulo rewrite instances | Jason Gross | 2016-07-29 |
* | Add some lemmas and hints about Zmod | Jason Gross | 2016-07-29 |
* | Add a zutil lemma | Jason Gross | 2016-07-29 |
* | Add instances to decide equality of sigma types | Jason Gross | 2016-07-29 |
* | Remove some lemmas that make things slower in Util/HProp | Jason Gross | 2016-07-29 |
* | Add a lemma about hprop and eq | Jason Gross | 2016-07-29 |
* | Make IsIso a class | Jason Gross | 2016-07-29 |
* | Add HProp, Isomorphism | Jason Gross | 2016-07-29 |
* | Add inversion helper tactics to Sigma.v | Jason Gross | 2016-07-29 |
* | Rename path_sig{,T}{ => _uncurried}_iff | Jason Gross | 2016-07-29 |
* | Add path_sig{,T}_iff | Jason Gross | 2016-07-29 |
* | Add some lemmas to Util.Sigma | Jason Gross | 2016-07-29 |
* | Set Asymmetric Patterns, add util lemmas about sig | Jason Gross | 2016-07-29 |
* | Get rid of unparsable unicode notation | Jason Gross | 2016-07-28 |
* | Add more reserved notations | Jason Gross | 2016-07-28 |
* | Add instances about congruence modulo | Jason Gross | 2016-07-28 |
* | Add unicode reserved notations | Jason Gross | 2016-07-28 |
* | Add Z.mod_mod to zsimplify | Jason Gross | 2016-07-28 |
* | Move most notation level declarations into Util | Jason Gross | 2016-07-27 |
* | Restore functionality of Z.simplify_fractions_le | Jason Gross | 2016-07-27 |
* | Make Z.pre_reorder_fractions / Z.simplify_fractions_le not loop | Jason Gross | 2016-07-27 |