diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-04 20:15:21 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-04 20:15:21 -0400 |
| commit | 68e353e45ad159d746baa629fcff246ca392098a (patch) | |
| tree | 42727214489e8cba69bb1a4fac1eb8547d8a9d0a /src/Util/ZUtil.v | |
| parent | 4cd73fac4f8f68bf390f8c87f27fa4cba3e68cef (diff) | |
Handle 0 mod _ in push_Zmod
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 624e953f9..f81f04076 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -100,7 +100,7 @@ Hint Rewrite <- Z.div_div using zutil_arith : push_Zdiv. Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using zutil_arith : pull_Zmod. Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod. Hint Rewrite Z_mod_nz_opp_full using zutil_arith : push_Zmod. -Hint Rewrite Z_mod_same_full : push_Zmod. +Hint Rewrite Z_mod_same_full Zmod_0_l : push_Zmod. Hint Rewrite Nat2Z.id : zsimplify. Hint Rewrite Nat2Z.id : push_Zof_nat. Hint Rewrite Nat2Z.inj_0 Nat2Z.inj_succ Nat2Z.inj_abs_nat Nat2Z.inj_add Nat2Z.inj_mul Nat2Z.inj_sub_max Nat2Z.inj_pred_max Nat2Z.inj_min Nat2Z.inj_max Zabs2Nat.id_abs Zabs2Nat.id : push_Zof_nat. @@ -2492,8 +2492,6 @@ End BoundsTactics. Ltac push_Zmod := repeat match goal with | _ => progress autorewrite with push_Zmod - | [ |- context[?x mod ?x] ] - => rewrite (Z_mod_same_full x) | [ |- context[(?x * ?y) mod ?z] ] => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod @@ -2513,8 +2511,6 @@ Ltac push_Zmod := Ltac push_Zmod_hyps := repeat match goal with | _ => progress autorewrite with push_Zmod in * |- - | [ H : context[?x mod ?x] |- _ ] - => rewrite (Z_mod_same_full x) in H | [ H : context[(?x * ?y) mod ?z] |- _ ] => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod |