Commit 7fe093db authored by François Bobot's avatar François Bobot

Merge branch 'stable'

accept also camlp4 (not only camlp5) for coq plugin compilation

Conflicts:
	Makefile.in
	configure.in
parents 6fe88dfc 3d9c9c8e
......@@ -47,7 +47,8 @@ OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
COQC = @COQC@
COQDEP = @COQDEP@
CAMLP5O = @CAMLP5O@
COQCAMLP = @COQCAMLP@
COQCAMLPLIB = @COQCAMLPLIB@
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
ifeq (@enable_menhirLib@,yes)
......@@ -768,7 +769,7 @@ COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel interp intf lib library parsing pretyping proofs printing tactics toplevel
COQPINCLUDES = -I src/coq-tactic -I +camlp5 $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
$(COQPCMO) $(COQPCMX): INCLUDES += $(COQPINCLUDES)
......@@ -795,8 +796,8 @@ lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(OCAMLC) -a $(BFLAGS) -o $@ $^
src/coq-tactic/why3tac.ml: src/coq-tactic/why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
$(CAMLP5O) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
$(if $(QUIET),@echo 'Camlp $<' &&) \
$(COQCAMLP) pr_dump.cmo @COQPPLIBS@ pa_macro.cmo -D@coq_compat_version@ -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
......
......@@ -275,8 +275,6 @@ if test "$MENHIR" = no ; then
AC_MSG_ERROR(Cannot find menhir.)
fi
AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
## Where are the library we need
# we look for ocamlfind; if not present, we just don't use it to find
# libraries
......@@ -496,6 +494,10 @@ else
AC_MSG_CHECKING(Coq version)
COQVERSION=`$COQC -v | sed -n -e 's|.*version* *\([[^ ]]*\) .*$|\1|p' `
#Even if the name of the variable is CAMLP4 the value can be camlp5
COQCAMLP=$(eval `coqtop -config`; echo ${CAMLP4BIN}${CAMLP4}o)
COQCAMLPLIB=$(eval `coqtop -config`; echo ${CAMLP4LIB})
case $COQVERSION in
8.4*)
enable_coq_support=yes
......@@ -730,7 +732,8 @@ AC_SUBST(MENHIR)
AC_SUBST(enable_profiling)
AC_SUBST(enable_bin_annot)
AC_SUBST(CAMLP5O)
AC_SUBST(COQCAMLP)
AC_SUBST(COQCAMLPLIB)
AC_SUBST(enable_ide)
AC_SUBST(LABLGTK2LIB)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment