diff options
author | Jason Gross <jagro@google.com> | 2016-07-08 08:57:18 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-08 08:57:18 -0700 |
commit | 7b34335b795fd3f27cb33526fb2dbe8677e67d6a (patch) | |
tree | 385cb55c2cc14e497528623de8a061455b0a7b69 /src/Util/ZUtil.v | |
parent | 72fd2095b56a6d39eb53c837aaf0098290a3dda7 (diff) |
Add Z.div_0_l to ZUtil
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 219165d08..64e07c99d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -22,7 +22,7 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z this database. *) Create HintDb zsimplify discriminated. Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify. -Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add using lia : zsimplify. +Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l using lia : zsimplify. (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) Create HintDb push_Zopp discriminated. |