aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common9
1 files changed, 5 insertions, 4 deletions
diff --git a/Makefile.common b/Makefile.common
index 96d0d2ed81..772561bd70 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -21,6 +21,7 @@ COQTOPEXE:=bin/coqtop$(EXE)
COQTOPBYTE:=bin/coqtop.byte$(EXE)
COQDEP:=bin/coqdep$(EXE)
+COQPP:=bin/coqpp$(EXE)
COQDEPBYTE:=bin/coqdep.byte$(EXE)
COQMAKEFILE:=bin/coq_makefile$(EXE)
COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE)
@@ -40,7 +41,7 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py
COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py
TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
- $(COQWORKMGR)
+ $(COQWORKMGR) $(COQPP)
TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\
$(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES)
@@ -88,13 +89,14 @@ INSTALLSH:=./install.sh
MKDIR:=install -d
CORESRCDIRS:=\
+ coqpp \
config clib lib kernel kernel/byterun library \
engine pretyping interp proofs parsing printing \
tactics vernac stm toplevel
PLUGINDIRS:=\
omega romega micromega quote \
- setoid_ring extraction fourier \
+ setoid_ring extraction \
cc funind firstorder derive \
rtauto nsatz syntax btauto \
ssrmatching ltac ssr
@@ -132,7 +134,6 @@ MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
QUOTECMO:=plugins/quote/quote_plugin.cmo
RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
-FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
FUNINDCMO:=plugins/funind/recdef_plugin.cmo
FOCMO:=plugins/firstorder/ground_plugin.cmo
@@ -153,7 +154,7 @@ SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
$(QUOTECMO) $(RINGCMO) \
- $(FOURIERCMO) $(EXTRACTIONCMO) \
+ $(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
$(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)