8.5 fixes

4 files changed, 11 insertions, 9 deletions

diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index cf3ebf29c..2d1ab6c58 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -1,12 +1,12 @@
-Require Import Coq.Arith.Arith.
+Require Import Coq.Arith.Arith Coq.Arith.Max.
 
 Ltac case_max :=
   match goal with [ |- context[max ?x ?y] ] =>
       destruct (le_dec x y);
       match goal with
-        | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by
+        | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by
           (exact H)
-        | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite Max.max_l by
+        | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite max_l by
           (exact (le_Sn_le _ _ (not_le _ _ H)))
       end
   end.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 6116312e1..82d22046d 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -1,5 +1,7 @@
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Require Import Coq.NArith.NArith Coq.PArith.BinPosDef.
+Require Import Coq.Numbers.Natural.Peano.NPeano.
+
 Local Open Scope equiv_scope.
 
 Generalizable All Variables.
@@ -147,7 +149,7 @@ Section IterAssocOp.
     destruct (funexp (test_and_op n a) (x, acc) y) as [i acc'].
     simpl in IHy.
     unfold test_and_op.
-    destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity.
+    destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity.
   Qed.
 
   Lemma iter_op_termination : forall sc a bound,
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 1f69b04d2..f86ecee2e 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,4 +1,5 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
+Import Nat.
 
 Local Open Scope nat_scope.
 
@@ -66,4 +67,3 @@ Proof.
     [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
     | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
 Qed.
-
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 1b7cfafdc..3ffc69fc5 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
 Require Import Coq.Lists.List.
+Import Nat.
 Local Open Scope Z.
 
 Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
@@ -208,7 +209,7 @@ Proof.
   rewrite (le_plus_minus n m) at 1 by assumption.
   rewrite Nat2Z.inj_add.
   rewrite Z.pow_add_r by apply Nat2Z.is_nonneg.
-  rewrite <- Z.div_div by first 
+  rewrite <- Z.div_div by first
     [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega
     | apply Z.pow_pos_nonneg; omega ].
   rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega).
@@ -345,7 +346,7 @@ Qed.
     + unfold Z.ones.
       rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r.
       omega.
-    + intros. 
+    + intros.
       destruct (Z_lt_le_dec x n); try omega.
       intuition.
       left.
@@ -360,7 +361,7 @@ Qed.
     Z.shiftr a i <= Z.ones (n - i) .
   Proof.
     intros a n i G G0 G1.
-    destruct (Z_le_lt_eq_dec i n G1). 
+    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).
@@ -415,4 +416,3 @@ Ltac zero_bounds := try omega; try prime_bound; zero_bounds'.
       zero_bounds.
       apply Z.pow_nonneg; omega.
   Qed.
-