Remove bbv dependency

2 files changed, 1 insertions, 32 deletions

diff --git a/default.nix b/default.nix
index 208db0a..e22a74c 100644
--- a/default.nix
+++ b/default.nix
@@ -2,35 +2,6 @@ with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/00197eff36bb
 let
   ncoq = coq_8_14;
   ncoqPackages = coqPackages_8_14;
-  bbv = ncoqPackages.callPackage
-    ( { coq, stdenv, fetchFromGithub, mkCoqDerivation }:
-      mkCoqDerivation {
-        pname = "bbv";
-        owner = "ymherklotz";
-
-        defaultVersion = "1.0-dev";
-
-        src = fetchFromGitHub {
-          owner = "mit-plv";
-          repo = "bbv";
-          rev = "d5ab9c04db85eb85688816dc687d118000a65736";
-          sha256 = "0qlgkzwrg80j50md9s3fbnq62xc7fx1cb9f3y8iz714824ihkhbj";
-        };
-
-        buildInputs = [ ];
-        propagatedBuildInputs = [ coq ];
-        enableParallelBuilding = true;
-
-        outputs = [ "out" ];
-
-        meta = with lib; {
-          description = "Bedrock Bit Vector Library";
-          homepage    = "https://github.com/mit-plv/bbv";
-          license     = licenses.mit;
-          platforms   = [ "x86_64-linux" "x86_64-darwin" ];
-          maintainers = [ ];
-        };
-      } ) { } ;
 in
 ncoqPackages.mkCoqDerivation {
   pname = "biteq";
@@ -39,7 +10,7 @@ ncoqPackages.mkCoqDerivation {
 
   src = ./.;
 
-  buildInputs = [ ncoq bbv ];
+  buildInputs = [ ncoq ];
 
   enableParallelBuilding = true;
 }
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; }.