diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-04 20:16:47 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-04 20:16:47 -0400 |
| commit | 230b316e11bc91a99c922f9ba1fee056f9eb98c7 (patch) | |
| tree | 17cf928574843cb13fdff05e3fb098303fa37539 /src/Util/ZUtil.v | |
| parent | 68e353e45ad159d746baa629fcff246ca392098a (diff) | |
Prevent infinite loops by not dealing with 0 mod _
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index f81f04076..bc37cb536 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 Zmod_0_l : push_Zmod. +Hint Rewrite Z_mod_same_full : 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. |