From 4483d41d6a510e01041f05546643934c9d2a887b Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@google.com>
Date: Fri, 26 Apr 2019 16:41:41 -0400
Subject: Remove bbv dependency

No code in fiat-crypto depends on bbv anymore, so delete it.

Closes https://github.com/mit-plv/fiat-crypto/issues/481.
---
 .gitmodules      |  3 ---
 Makefile         |  4 ++--
 _CoqProject      | 17 -----------------
 bbv              |  1 -
 etc/ci/travis.sh |  2 +-
 5 files changed, 3 insertions(+), 24 deletions(-)
 delete mode 160000 bbv

diff --git a/.gitmodules b/.gitmodules
index 0a919ab11..ff4ce384d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,6 @@
 [submodule "etc/coq-scripts"]
 	path = etc/coq-scripts
 	url = https://github.com/JasonGross/coq-scripts.git
-[submodule "bbv"]
-	path = bbv
-	url = ../../mit-plv/bbv.git
 [submodule "coqprime"]
 	path = coqprime
 	url = https://github.com/thery/coqprime
diff --git a/Makefile b/Makefile
index fbd3bed0d..cd07dad19 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ include etc/coq-scripts/Makefile.vo_closure
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq
 update-_CoqProject::
 	$(SHOW)'ECHO > _CoqProject'
-	$(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv/theories bbv'; ((git ls-files 'src/*.v'; (git submodule foreach 'git ls-files "*.v" 2>/dev/null | sed "s|^|$$path/|"' | grep 'bbv/')) | $(GREP_EXCLUDE_SPECIAL_VOFILES) | $(SORT_COQPROJECT))) > _CoqProject
+	$(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(GREP_EXCLUDE_SPECIAL_VOFILES) | $(SORT_COQPROJECT))) > _CoqProject
 
 # coq .vo files that are not compiled using coq_makefile
 SPECIAL_VOFILES := \
@@ -59,7 +59,7 @@ NOBIGMEM_UNMADE_VOFILES := \
 	src/Curves/Weierstrass/Projective.vo
 REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES),$(VOFILES))
 PRE_STANDALONE_PRE_VOFILES := $(filter src/Standalone%.vo,$(REGULAR_VOFILES))
-UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
+UTIL_PRE_VOFILES := $(filter src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
 SOME_EARLY_VOFILES := \
   src/Arithmetic/Core.vo \
   src/Rewriter.vo
diff --git a/_CoqProject b/_CoqProject
index 6e7e43e64..db7e7ba8e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,21 +1,4 @@
 -R src Crypto
--R bbv/theories bbv
-bbv/theories/BinNotation.v
-bbv/theories/BinNotationZ.v
-bbv/theories/DepEq.v
-bbv/theories/DepEqNat.v
-bbv/theories/HexNotation.v
-bbv/theories/HexNotationWord.v
-bbv/theories/HexNotationZ.v
-bbv/theories/NLib.v
-bbv/theories/N_Z_nat_conversions.v
-bbv/theories/NatLib.v
-bbv/theories/Nomega.v
-bbv/theories/ReservedNotations.v
-bbv/theories/Word.v
-bbv/theories/WordScope.v
-bbv/theories/ZHints.v
-bbv/theories/ZLib.v
 src/AbstractInterpretation.v
 src/AbstractInterpretationProofs.v
 src/AbstractInterpretationWf.v
diff --git a/bbv b/bbv
deleted file mode 160000
index 143c47ba1..000000000
--- a/bbv
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 143c47ba1267a0a700c17bdf5bbded9b6e4bfbb1
diff --git a/etc/ci/travis.sh b/etc/ci/travis.sh
index 8942d1db7..f16f0e555 100755
--- a/etc/ci/travis.sh
+++ b/etc/ci/travis.sh
@@ -13,7 +13,7 @@ rm -f finished.ok
 (make "$@" -j2 TIMED=1 2>&1 && touch finished.ok) | tee -a time-of-build.log
 python "./etc/coq-scripts/timing/make-one-time-file.py" "time-of-build.log" "time-of-build-pretty.log" || exit $?
 rm -f "${CUR_ARCHIVE}"
-tar -czf "${CUR_ARCHIVE}" time-of-build.log src bbv coqprime || exit $?
+tar -czf "${CUR_ARCHIVE}" time-of-build.log src coqprime || exit $?
 
 git update-index --assume-unchanged _CoqProject
 git status
-- 
cgit v1.2.3