| Commit message (Expand) | Author | Age |
* | 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 |
* | Add another ZUtil lemma | Jason Gross | 2016-07-26 |
* | Fix 8.6 build | Jason Gross | 2016-07-26 |
* | Fix 8.4 build. | jadep | 2016-07-25 |
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-07-25 |
|\ |
|
* | | Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change... | jadep | 2016-07-25 |
* | | A couple new util lemmas | jadep | 2016-07-25 |
| * | If COQPATH is not set, set it by default (#38) | Jason Gross | 2016-07-25 |
| * | In >= 8.6, disable some very noisy warnings | Jason Gross | 2016-07-25 |
| * | More Zpow in ZUtil | Jason Gross | 2016-07-22 |
| * | More ZUtil | Jason Gross | 2016-07-22 |
| * | Add databases for ring_simplify | Jason Gross | 2016-07-22 |
| * | Add reverse_nondep and ring_simplify_subterms_in_all tactics | Jason Gross | 2016-07-22 |
| * | More ZUtil lemmas | Jason Gross | 2016-07-22 |
| * | Revert "Revert "Add more ZUtil automation"" | Jason Gross | 2016-07-22 |
| * | Merge pull request #37 from JasonGross/fix-intuition | Jason Gross | 2016-07-22 |
| |\ |
|
| | * | Make the library 20% faster: [auto with *] is evil | Jason Gross | 2016-07-22 |
| | * | Revert "Add more ZUtil automation" | Jason Gross | 2016-07-22 |
| |/ |
|