diff options
| -rw-r--r-- | Makefile | 3 | ||||
| -rw-r--r-- | _CoqProject | 8 |
2 files changed, 3 insertions, 8 deletions
@@ -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 |