aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-04 11:01:13 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-04 11:01:13 +0000
commit7548c4c4baffdbb07b1edc59b1df2483506a1476 (patch)
tree4ecf9048461c582ed5ccf188097cef82981f2494 /src
parenta698c19127ee861c32e998b14b4ebc7e3a913fe0 (diff)
downloadbiteq-7548c4c4baffdbb07b1edc59b1df2483506a1476.tar.gz
biteq-7548c4c4baffdbb07b1edc59b1df2483506a1476.zip
Remove bbv dependency
Diffstat (limited to 'src')
-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; }.