aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Util.Equality on 8.4Gravatar Andres Erbsen2016-08-04
* prove an admitGravatar Andres Erbsen2016-08-04
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* More zsimplifyGravatar Jason Gross2016-08-03
* Add some autogenerated zsimplify lemmasGravatar Jason Gross2016-08-03
* Better Zmod manipulationGravatar Jason Gross2016-08-03
* Remove Bool.absorption_andb Bool.absorption_orb, not present in < 8.4pl5Gravatar Jason Gross2016-08-03
* Weaken some ZUtil assumptionsGravatar Jason Gross2016-08-03
* More ZUtilGravatar Jason Gross2016-08-03
* More ZUtilGravatar Jason Gross2016-08-03
* Add ZUtil lemmas, and Util.BoolGravatar Jason Gross2016-08-03
* More zsimplify hintsGravatar Jason Gross2016-08-03
* Add {push,pull}_Zdiv databasesGravatar Jason Gross2016-08-03
* Add more ZUtil lemmasGravatar Jason Gross2016-08-03
* Add some simplification lemmas to ZUtilGravatar Jason Gross2016-08-02
* Add pull_Zmod tacticGravatar Jason Gross2016-08-01
* Make Z.ltb_to_lt more powerfulGravatar Jason Gross2016-08-01
* Add div lower/upper bounds to zarith hint dbGravatar Jason Gross2016-08-01
* Better hint for div_to_inv_moduloGravatar Jason Gross2016-08-01
* Add a commentGravatar Jason Gross2016-08-01
* Better transparency of dec_eq_sig_hpropGravatar Jason Gross2016-08-01
* Add a lemma about removing division in modular arithmeticGravatar Jason Gross2016-08-01
* Add documentation: Equality, HProp, Isomorphism, Sigma (#41)Gravatar Jason Gross2016-08-01
* Fixes for Coq 8.4Gravatar Jason Gross2016-08-01
* Add [0 mod _ = 0] to zsimplify dbGravatar Jason Gross2016-08-01
* Add a tactic to eliminate hprop trivial proofsGravatar Jason Gross2016-08-01
* Remove useless hypotheses for [path_sigT_uncurried_iff]Gravatar Jason Gross2016-08-01
* Add push_Zmod tacticsGravatar Jason Gross2016-07-29
* Don't give equiv_modulo reflexive instance priority over eqGravatar Jason Gross2016-07-29
* Add more Z.modulo lemmasGravatar Jason Gross2016-07-29
* Add another ZUtil rewrite hintGravatar Jason Gross2016-07-29
* Add a ZUtil rewrite hintGravatar Jason Gross2016-07-29
* Add equiv_modulo rewrite instancesGravatar Jason Gross2016-07-29
* Add some lemmas and hints about ZmodGravatar Jason Gross2016-07-29
* Add a zutil lemmaGravatar Jason Gross2016-07-29
* Add instances to decide equality of sigma typesGravatar Jason Gross2016-07-29
* Remove some lemmas that make things slower in Util/HPropGravatar Jason Gross2016-07-29
* Add a lemma about hprop and eqGravatar Jason Gross2016-07-29
* Make IsIso a classGravatar Jason Gross2016-07-29
* Add HProp, IsomorphismGravatar Jason Gross2016-07-29
* Add inversion helper tactics to Sigma.vGravatar Jason Gross2016-07-29
* Rename path_sig{,T}{ => _uncurried}_iffGravatar Jason Gross2016-07-29
* Add path_sig{,T}_iffGravatar Jason Gross2016-07-29
* Add some lemmas to Util.SigmaGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
* Get rid of unparsable unicode notationGravatar Jason Gross2016-07-28
* Add more reserved notationsGravatar Jason Gross2016-07-28
* Add instances about congruence moduloGravatar Jason Gross2016-07-28
* Add unicode reserved notationsGravatar Jason Gross2016-07-28
* Add Z.mod_mod to zsimplifyGravatar Jason Gross2016-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 08:16:01 +0000