aboutsummaryrefslogtreecommitdiffstats
path: root/src/BitEQ.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/BitEQ.v')
-rw-r--r--src/BitEQ.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/BitEQ.v b/src/BitEQ.v
index 35d08aa..4689b26 100644
--- a/src/BitEQ.v
+++ b/src/BitEQ.v
@@ -5,8 +5,6 @@ Require Import Coq.Bool.Bool.
Require Import biteq.Lib.
-Require Import bbv.Word.
-
#[local] Open Scope Z_scope.
Record bv := Zbv { size: N; val: Z; }.