From 7548c4c4baffdbb07b1edc59b1df2483506a1476 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 4 Mar 2022 11:01:13 +0000
Subject: Remove bbv dependency

---
 default.nix | 31 +------------------------------
 src/BitEQ.v |  2 --
 2 files changed, 1 insertion(+), 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; }.
-- 
cgit