From f626f41c8c5df7eb4131d16f8cc6e05140fd509c Mon Sep 17 00:00:00 2001 From: Jason Gross 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 --- _CoqProject | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to '_CoqProject') 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