diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-28 22:28:45 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-28 22:28:45 -0400 |
| commit | 16b20d1a51acb3ebc7b4b8c92a9940d1b73431c9 (patch) | |
| tree | 1766c1e76c153d0143e796adc0085c22486923fa /src/Util/ZUtil.v | |
| parent | b2f706d6d391666b282f8a65a993275f63a38a72 (diff) | |
Add Z.one_succ Z.two_succ to zsimplify_const db
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 38709174e..88370e533 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -58,6 +58,7 @@ Hint Rewrite <- Z.opp_eq_mul_m1 Z.one_succ Z.two_succ : zsimplify. Hint Rewrite <- Z.div_mod using zutil_arith : zsimplify. Hint Rewrite (fun x y => proj2 (Z.eqb_neq x y)) using assumption : zsimplify. Hint Rewrite Z.mul_0_l Z.mul_0_r Z.mul_1_l Z.mul_1_r Z.add_0_l Z.add_0_r Z.sub_0_l Z.sub_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_0_l Zmod_0_r Zmod_1_r Z.opp_0 : zsimplify_const. +Hint Rewrite <- Z.one_succ Z.two_succ : zsimplify_const. (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) Create HintDb push_Zopp discriminated. |