From 16b20d1a51acb3ebc7b4b8c92a9940d1b73431c9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Mar 2017 22:28:45 -0400 Subject: Add Z.one_succ Z.two_succ to zsimplify_const db --- src/Util/ZUtil.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Util/ZUtil.v') 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. -- cgit v1.2.3