aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-01 22:29:31 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-04-02 10:28:13 -0400
commit7565295b8bd446004aa8cc19b86184a331022597 (patch)
treedebdb87dc7d56ca89aed89977e9f61b27ffd81b4 /Makefile
parent39423861f916252b9d42eb40c3198a65d31ee410 (diff)
Remove all the .v files in SpecificGen
This gets most of the way to 10 in #14.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 1 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index 34abc03f0..0c73a0897 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,6 @@ HIDE := $(if $(VERBOSE),,@)
install-coqprime clean-coqprime coqprime \
specific-display display \
specific non-specific \
- small-specific-gen medium-specific-gen specific-gen \
extraction ghc
SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
@@ -54,20 +53,13 @@ HEAVY_VOFILES := src/WeierstrassCurve/WeierstrassCurveTheorems.vo
COQ_VOFILES := $(filter-out $(UNMADE_VOFILES),$(VOFILES))
LITE_VOFILES := $(filter-out $(HEAVY_VOFILES),$(COQ_VOFILES))
SPECIFIC_VO := $(filter src/Specific/%,$(VOFILES))
-SPECIFIC_GEN_VO := $(filter src/SpecificGen/%,$(VOFILES))
-MEDIUM_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF5211_32%,$(SPECIFIC_GEN_VO))
-SMALL_SPECIFIC_GEN_VO := $(filter-out src/SpecificGen/GF41417_32%,$(MEDIUM_SPECIFIC_GEN_VO))
NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(VO_FILES))
SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(VOFILES))
-SPECIFIC_GEN_DISPLAY_VO := $(filter src/SpecificGen/%Display.vo,$(VOFILES))
-DISPLAY_VO := $(SPECIFIC_DISPLAY_VO) $(SPECIFIC_GEN_DISPLAY_VO)
+DISPLAY_VO := $(SPECIFIC_DISPLAY_VO)
DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO))
DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
specific: $(SPECIFIC_VO) coqprime
-specific-gen: $(SPECIFIC_GEN_VO) coqprime
-medium-specific-gen: $(MEDIUM_SPECIFIC_GEN_VO) coqprime
-small-specific-gen: $(SMALL_SPECIFIC_GEN_VO) coqprime
non-specific: $(NON_SPECIFIC_VO) coqprime
specific-display: $(SPECIFIC_DISPLAY_VO:.vo=.log) coqprime
display: $(DISPLAY_VO:.vo=.log) coqprime