aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index c62795319..6e9ccbb4d 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ INSTALLDEFAULTROOT := Crypto
old-pipeline-lite print-old-pipeline-lite \
coq-without-new-pipeline \
nobigmem print-nobigmem \
- util \
+ util some-early \
specific-c specific-display display \
specific non-specific lite only-heavy printlite lite-display print-lite-display \
new-pipeline pre-standalone \
@@ -117,6 +117,10 @@ NEW_PIPELINE_PRE_VOFILES := $(filter $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
PRE_STANDALONE_PRE_VOFILES := $(filter src/Experiments/NewPipeline/Standalone%.vo,$(REGULAR_VOFILES))
UTIL_PRE_VOFILES := $(filter bbv/%.vo src/Algebra/%.vo src/Tactics/%.vo src/Util/%.vo,$(REGULAR_VOFILES))
COQ_WITHOUT_NEW_PIPELINE_VOFILES := $(filter-out $(NEW_PIPELINE_FILTER),$(REGULAR_VOFILES))
+SOME_EARLY_VOFILES := \
+ src/Experiments/NewPipeline/Arithmetic.vo \
+ src/Experiments/NewPipeline/Rewriter.vo \
+ src/Experiments/SimplyTypedArithmetic.vo
SELECTED_PATTERN := \
src/Specific/X25519/C64/% \
@@ -206,6 +210,7 @@ specific-c: $(filter-out $(UNMADE_C_FILES),$(SPECIFIC_DISPLAY_VO:Display.vo=.c)
selected-specific: $(SELECTED_SPECIFIC_VOFILES)
selected-specific-display: $(SELECTED_SPECIFIC_DISPLAY_VO:.vo=.log)
selected-c: $(filter-out $(UNMADE_C_FILES),$(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(SELECTED_SPECIFIC_DISPLAY_VO:Display.vo=.h))
+some-early: $(SOME_EARLY_VOFILES)
nonautogenerated-specific: $(NONAUTOGENERATED_SPECIFIC_VOFILES)
nonautogenerated-specific-display: $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:.vo=.log)
nonautogenerated-c: $(filter-out $(UNMADE_C_FILES),$(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.c) $(NONAUTOGENERATED_SPECIFIC_DISPLAY_VO:Display.vo=.h))