diff options
| -rw-r--r-- | Bedrock/Word.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 1744f80ef..2c518807d 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -1,6 +1,6 @@ (** Fixed precision machine words *) -Require Import Coq.ZArith.ZArith Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega. +Require Import Coq.Arith.Arith Coq.Arith.Div2 Coq.NArith.NArith Coq.Bool.Bool Coq.omega.Omega. Require Import Bedrock.Nomega. Set Implicit Arguments. @@ -84,9 +84,6 @@ Definition NToWord (sz : nat) (n : N) : word sz := | Npos p => posToWord sz p end. -Definition ZToWord sz (n : Z) : word sz := NToWord sz (Z.to_N n). -Definition wordToZ sz (w : word sz) : Z := Z.of_N (wordToN w). - Fixpoint Npow2 (n : nat) : N := match n with | O => 1 |