aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-08 03:11:06 +0100
committerEmilio Jesus Gallego Arias2018-11-21 17:15:28 +0100
commitaa151dbc7aa501bac78b835a80f9a25c5316d2dc (patch)
tree16960e510f0effe439d4839626e0be692b9f6355 /tools
parentabcc20d6a3aebee36160cd17b1f80c56f39876f3 (diff)
[camlp5] Remove dependency on camlp5.
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in22
1 files changed, 1 insertions, 21 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 0d1629c3d5..b673225e40 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -20,7 +20,6 @@ include @CONF_FILE@
VFILES := $(COQMF_VFILES)
MLIFILES := $(COQMF_MLIFILES)
MLFILES := $(COQMF_MLFILES)
-ML4FILES := $(COQMF_ML4FILES)
MLGFILES := $(COQMF_MLGFILES)
MLPACKFILES := $(COQMF_MLPACKFILES)
MLLIBFILES := $(COQMF_MLLIBFILES)
@@ -37,10 +36,6 @@ LOCAL := $(COQMF_LOCAL)
COQLIB := $(COQMF_COQLIB)
DOCDIR := $(COQMF_DOCDIR)
OCAMLFIND := $(COQMF_OCAMLFIND)
-CAMLP5O := $(COQMF_CAMLP5O)
-CAMLP5BIN := $(COQMF_CAMLP5BIN)
-CAMLP5LIB := $(COQMF_CAMLP5LIB)
-CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS)
CAMLFLAGS := $(COQMF_CAMLFLAGS)
HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
@@ -192,22 +187,11 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
-CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB)
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS)
# ocamldoc fails with unknown argument otherwise
CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS)))
-# FIXME This should be generated by Coq
-GRAMMARS:=grammar.cma
-CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
-
-CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null)
-ifeq (,$(CAMLLIB))
-PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.")
-else
-PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl'
-endif
-
ifneq (,$(TIMING))
TIMING_ARG=-time
ifeq (after,$(TIMING))
@@ -774,10 +758,6 @@ printenv::
@echo 'COQLIB = $(COQLIB)'
@echo 'DOCDIR = $(DOCDIR)'
@echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'CAMLP5O = $(CAMLP5O)'
- @echo 'CAMLP5BIN = $(CAMLP5BIN)'
- @echo 'CAMLP5LIB = $(CAMLP5LIB)'
- @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)'
@echo 'HASNATDYNLINK = $(HASNATDYNLINK)'
@echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)'
@echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)'