From f626f41c8c5df7eb4131d16f8cc6e05140fd509c Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 11 Apr 2019 13:10:30 -0400
Subject: Don't include extraction .vo files in the all target

We run coqc on these files via the c-files target, which is also
included in the all target
---
 Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 17d57cb07..fbd3bed0d 100644
--- a/Makefile
+++ b/Makefile
@@ -37,12 +37,13 @@ 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/')) | $(SORT_COQPROJECT))) > _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
 
 # coq .vo files that are not compiled using coq_makefile
 SPECIAL_VOFILES := \
 	src/ExtractionOCaml/%.vo \
 	src/ExtractionHaskell/%.vo
+GREP_EXCLUDE_SPECIAL_VOFILES := grep -v '^src/Extraction\(OCaml\|Haskell\)/'
 # add files to this list to prevent them from being built as final
 # targets by the "lite" target
 LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
-- 
cgit v1.2.3