minor updates needed to make it compile with bbv

removing lemma wordToNat_wzero is ok because it's already in bbv

4 files changed, 7 insertions, 13 deletions

diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
index 2befc1ef6..10a7d78ff 100644
--- a/src/Util/FixedWordSizes.v
+++ b/src/Util/FixedWordSizes.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.BinNat.
 Require Import Coq.Arith.Arith.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 
 Definition word32 := word 32. (* 2^5 *)
 Definition word64 := word 64. (* 2^6 *)
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index f699adeed..bd71f5b80 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.NArith.BinNat.
 Require Import Coq.Arith.Arith.
-Require Import Bedrock.Word.
+Require Import bbv.WordScope.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.WordUtil.
 Require Import Crypto.Util.ZUtil.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 9321f2b23..8c354690b 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -1,7 +1,8 @@
 Require Import Coq.NArith.NArith.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Util.NatUtil Crypto.Util.Decidable.
-Require Bedrock.Word.
+Require bbv.WordScope.
+Require Import bbv.NatLib.
 Require Crypto.Util.WordUtil.
 
 Module N.
@@ -107,7 +108,7 @@ Module N.
   Section ZN.
     Import Coq.ZArith.ZArith.
     Lemma ZToN_NPow2_lt : forall z n, (0 <= z < 2 ^ Z.of_nat n)%Z ->
-                                      (Z.to_N z < Word.Npow2 n)%N.
+                                      (Z.to_N z < Npow2 n)%N.
     Proof.
       intros.
       apply WordUtil.bound_check_nat_N.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 64cfda434..c1eeb138b 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -15,8 +15,8 @@ Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Sigma.
 
-Require Import Bedrock.Word.
-Require Import Bedrock.Nomega.
+Require Import bbv.WordScope.
+Require Import bbv.Nomega.
 
 Require Import Crypto.Util.FixCoqMistakes.
 
@@ -370,8 +370,6 @@ Section WordToN.
       + clear IHk'.
         shatter x; simpl.
 
-        rewrite N.succ_double_spec; simpl.
-
         rewrite kill_match.
         replace (N.pos (Pos.of_succ_nat k'))
            with (N.succ (N.of_nat k'))
@@ -826,11 +824,6 @@ Definition setbit {b} n {H:n < b} (w:word b) : word b :=
 Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
   wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
 
-Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0.
-Proof.
-  unfold wzero; induction n as [|n IHn]; simpl; try rewrite_hyp!*; omega.
-Qed.
-
 Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
   wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
 Proof.