aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 10:07:47 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-19 10:07:47 +0100
commit1cf756712b5a5216e3a0039fb9d831c8d8ba9cbf (patch)
tree1cadeb96cce15c51dd6ffd217e3242657a11d70f /tools
parent8e9d1421354d55bc2ea71e37715a19d33cc9bc9c (diff)
parentb60906cc3ee3f994babf9cceff2971bd03485f2f (diff)
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use camlp4
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in28
1 files changed, 11 insertions, 17 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 23212ef84..727fd3ec3 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -34,11 +34,10 @@ LOCAL := $(COQMF_LOCAL)
COQLIB := $(COQMF_COQLIB)
DOCDIR := $(COQMF_DOCDIR)
OCAMLFIND := $(COQMF_OCAMLFIND)
-CAMLP4 := $(COQMF_CAMLP4)
-CAMLP4O := $(COQMF_CAMLP4O)
-CAMLP4BIN := $(COQMF_CAMLP4BIN)
-CAMLP4LIB := $(COQMF_CAMLP4LIB)
-CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS)
+CAMLP5O := $(COQMF_CAMLP5O)
+CAMLP5BIN := $(COQMF_CAMLP5BIN)
+CAMLP5LIB := $(COQMF_CAMLP5LIB)
+CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS)
CAMLFLAGS := $(COQMF_CAMLFLAGS)
HASNATDYNLINK := $(COQMF_HASNATDYNLINK)
@@ -179,24 +178,20 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)")
-CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
+CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB)
# 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
-ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
-else
-CAMLP4EXTEND=
-endif
+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 '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
+PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl'
endif
ifneq (,$(TIMING))
@@ -752,11 +747,10 @@ printenv::
@echo 'COQLIB = $(COQLIB)'
@echo 'DOCDIR = $(DOCDIR)'
@echo 'OCAMLFIND = $(OCAMLFIND)'
- @echo 'CAMLP4 = $(CAMLP4)'
- @echo 'CAMLP4O = $(CAMLP4O)'
- @echo 'CAMLP4BIN = $(CAMLP4BIN)'
- @echo 'CAMLP4LIB = $(CAMLP4LIB)'
- @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)'
+ @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)'