From cd496376a5f237340d7daff1bae8f23004d5358a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 3 Jan 2017 14:09:42 -0500 Subject: Revert "Add Bedrock.Word.{wordToZ,ZToWord}" This reverts commit a66ba3e5202adcc436c3a1fcf6433261e7bdd158. --- Bedrock/Word.v | 5 +---- 1 file changed, 1 insertion(+), 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 -- cgit v1.2.3