aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
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