diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-03-07 12:51:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-03-07 12:51:06 -0500 |
| commit | 291dcc2fd37e2338aafa5f5d9c5db70c2af07c12 (patch) | |
| tree | 02e7fac5ddb2d69cb712aa022f7e690428a9ec7c /src/Util/ZUtil.v | |
| parent | db92a67edea0400c3701109eb30b515f4292763f (diff) | |
Don't use deprecated compat notations in ZUtil
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 50ac909e1..eab5fda1b 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -170,7 +170,7 @@ Module Z. Proof. intros i ?. apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption; - (destruct (Z_eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; + (destruct (Z.eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; replace a with 0 by omega; f_equal; ring | ]); try omega. rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. replace (Z.succ x - n) with (x - (n - 1)) by ring. @@ -346,7 +346,7 @@ Module Z. destruct (Z_le_lt_eq_dec i n G1). + destruct (Z.shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. - destruct (Z_eq_dec a 0). + destruct (Z.eq_dec a 0). - subst; rewrite Z.shiftr_0_l; reflexivity. - rewrite Z.shiftr_eq_0; try omega; try reflexivity. apply Z.log2_lt_pow2; omega. @@ -358,7 +358,7 @@ Module Z. intros a ? ? [a_nonneg a_upper_bound]. apply Z_le_lt_eq_dec in a_upper_bound. destruct a_upper_bound. - + destruct (Z_eq_dec 0 a). + + destruct (Z.eq_dec 0 a). - subst; rewrite Z.shiftr_0_l; omega. - rewrite Z.shiftr_eq_0; auto; try omega. apply Z.log2_lt_pow2; auto; omega. @@ -580,7 +580,7 @@ Module Z. Lemma compare_add_shiftl : forall x1 y1 x2 y2 n, 0 <= n -> Z.pow2_mod x1 n = x1 -> Z.pow2_mod x2 n = x2 -> x1 + (y1 << n) ?= x2 + (y2 << n) = - if Z_eq_dec y1 y2 + if Z.eq_dec y1 y2 then x1 ?= x2 else y1 ?= y2. Proof. |