Commit 3d9c9c8e authored by François Bobot's avatar François Bobot

[Makefile] compile even if coq use camlp4 instead of camlp5

parent 88004948
......@@ -47,7 +47,8 @@ OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
COQC = @COQC@
COQDEP = @COQDEP@
CAMLP5O = @CAMLP5O@
COQCAMLP = @COQCAMLP@
COQCAMLPLIB = @COQCAMLPLIB@
FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
DEPFLAGS = -slash -I lib/why3
......@@ -755,7 +756,7 @@ COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = kernel lib interp parsing proofs pretyping tactics library 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)
......@@ -779,8 +780,8 @@ lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
$(OCAMLC) -a $(BFLAGS) -o $@ $(addsuffix .cma, @ZIPLIB@) $^
src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
$(if $(QUIET),@echo 'Camlp5 $<' &&) \
$(CAMLP5O) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
$(if $(QUIET),@echo 'Camlp $<' &&) \
$(COQCAMLP) pr_o.cmo @COQLIB@/parsing/grammar.cma -impl $^ -o $@
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cma
$(if $(QUIET),@echo 'Coqc $<' &&) \
......
......@@ -279,8 +279,6 @@ else
fi
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
......@@ -466,6 +464,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*|trunk)
enable_coq_support=yes
......@@ -701,7 +703,8 @@ dnl AC_SUBST(OCAMLWEB)
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