From 3fd5f652ba38a0b308b6e2e86783d82b861fb5bf Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Fri, 2 Feb 2018 16:09:01 -0500
Subject: minor updates needed to make it compile with bbv

removing lemma wordToNat_wzero is ok because it's already in bbv
---
 src/Util/NUtil.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/Util/NUtil.v')

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.
-- 
cgit v1.2.3