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 ++-
 _CoqProject | 8 +-------
 2 files changed, 3 insertions(+), 8 deletions(-)

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 \
diff --git a/_CoqProject b/_CoqProject
index 4d4b652ff..8859f08ed 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,9 +35,9 @@ src/MiscCompilerPasses.v
 src/MiscCompilerPassesProofs.v
 src/PreLanguage.v
 src/Rewriter.v
-src/RewriterInterpProofs1.v
 src/RewriterAll.v
 src/RewriterAllTactics.v
+src/RewriterInterpProofs1.v
 src/RewriterRules.v
 src/RewriterRulesProofs.v
 src/RewriterWf1.v
@@ -91,12 +91,6 @@ src/Curves/Weierstrass/Affine.v
 src/Curves/Weierstrass/AffineProofs.v
 src/Curves/Weierstrass/Jacobian.v
 src/Curves/Weierstrass/Projective.v
-src/ExtractionHaskell/saturated_solinas.v
-src/ExtractionHaskell/unsaturated_solinas.v
-src/ExtractionHaskell/word_by_word_montgomery.v
-src/ExtractionOCaml/saturated_solinas.v
-src/ExtractionOCaml/unsaturated_solinas.v
-src/ExtractionOCaml/word_by_word_montgomery.v
 src/Fancy/Barrett256.v
 src/Fancy/Compiler.v
 src/Fancy/Montgomery256.v
-- 
cgit v1.2.3