Prise en compte camlp4.opt dans la configuration et le Makefile

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@844 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 24 insertions, 17 deletions

diff --git a/Makefile b/Makefile
index 3579cba7eb..38f82bb909 100644
--- a/Makefile
+++ b/Makefile
@@ -39,9 +39,9 @@ OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
 OCAMLDEP=ocamldep
 DEPFLAGS=$(LOCALINCLUDES)
 
-OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
-OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
-CAMLP4O=camlp4o -I . pa_extend.cmo q_MLast.cmo
+OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
+OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
+CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo
 CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
 
 COQINCLUDES=-I states -I contrib/omega -I contrib/ring -I contrib/xml \
@@ -72,9 +72,9 @@ KERNEL=kernel/names.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/cooking.cmo kernel/safe_typing.cmo
 
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
-	library/goptions.cmo \
+	library/goptions.cmo library/nametab.cmo \
 	library/global.cmo library/library.cmo library/states.cmo \
-	library/nametab.cmo library/impargs.cmo \
+	library/impargs.cmo \
         library/indrec.cmo library/declare.cmo 
 
 PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \
@@ -522,13 +522,13 @@ toplevel/mltop.cmx: toplevel/mltop.optml
 	$(OCAMLOPT) $(OPTFLAGS) -c -impl toplevel/mltop.optml -o $@
 
 toplevel/mltop.byteml: toplevel/mltop.ml4
-	$(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@
 
 toplevel/mltop.optml: toplevel/mltop.ml4
-	$(CAMLP4O) pr_o.cmo pa_ifdef.cmo -impl toplevel/mltop.ml4 > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo pa_ifdef.cmo -impl toplevel/mltop.ml4 > $@ || rm -f $@
 
 toplevel/mltop.ml: toplevel/mltop.ml4
-	$(CAMLP4O) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo pa_ifdef.cmo -DByte -impl toplevel/mltop.ml4 > $@ || rm -f $@
 
 ML4FILES += toplevel/mltop.ml4
 
@@ -554,13 +554,13 @@ clean::
 	ocamllex $<
 
 .ml4.cmo:
-	$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+	$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
 
 .ml4.cmx:
-	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
+	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
 
 .ml4.ml:
-	$(CAMLP4O) pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@ || rm -f $@
 
 .v.vo:
 	$(COQC) -q -$(BEST) -bindir bin $(COQINCLUDES) $<
diff --git a/config/Makefile.template b/config/Makefile.template
index 07e9089c85..62dae6b803 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -42,6 +42,7 @@ CAMLBIN=CAMLBINDIRECTORY
 CAMLP4BIN=CAMLP4BINDIRECTORY
 
 # Camlp4 library directory
+CAMLP4O=CAMLP4TOOL
 CAMLP4LIB=CAMLP4LIBDIRECTORY
 
 # Objective-Caml compile command 
diff --git a/configure b/configure
index ec815942a8..b1970af292 100755
--- a/configure
+++ b/configure
@@ -23,6 +23,7 @@ done
 
 bytecamlc=ocamlc
 nativecamlc=ocamlopt
+camlp4o=camlp4o
 coq_debug_flag=
 coq_profile_flag=
 best_compiler=opt
@@ -80,6 +81,7 @@ while : ; do
                   arch=$2
 		  shift;;
     -opt|--opt) bytecamlc=ocamlc.opt
+                camlp4o=camlp4o.opt
                 nativecamlc=ocamlopt.opt;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
@@ -297,18 +299,20 @@ CAMLLIB=`ocamlc -v | sed -n -e 's|.*directory:* *\(.*\)$|\1|p' `
 
 # Camlp4
 
-CAMLP4=`which camlp4`
+CAMLP4=`which $camlp4o`
 case $CAMLP4 in
 	"") echo "camlp4 is not present in your path!"
 	echo "Give me manually the path to the camlp4 executable [/usr/local/bin by default]: "
 	read CAMLP4
 	
 	case $CAMLP4 in
-		"") CAMLP4=/usr/local/bin/camlp4;;
-		*/camlp4) true;;
-		*/) CAMLP4=${CAMLP4}camlp4;;
-		*) CAMLP4=${CAMLP4}/camlp4;;
-	esac;;
+		"") CAMLP4=/usr/local/bin/camlp4o;;
+		*/camlp4) CAMLP4=${CAMLP4}o;;
+		*/camlp4o) true;;
+		*/) CAMLP4=${CAMLP4}camlp4o;;
+		*) CAMLP4=${CAMLP4}/camlp4o;;
+	esac
+	camlp4o=$CAMLP4;;
 esac
 
 if test ! -f $CAMLP4 ; then
@@ -394,6 +398,7 @@ case $ARCH in
 	    -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
 	    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
 	    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+	    -e "s|CAMLP4TOOL|$camlp4o|" \
 	    -e "s|OSKIND|$OSTYPE|" \
 	    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
 	    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \
@@ -419,6 +424,7 @@ case $ARCH in
 	    -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
 	    -e "s|CAMLP4BINDIRECTORY|$CAMLP4BIN|" \
 	    -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \
+	    -e "s|CAMLP4TOOL|$camlp4o|" \
 	    -e "s|OSKIND|$OSTYPE|" \
 	    -e "s|COQDEBUGFLAG|$coq_debug_flag|" \
 	    -e "s|COQPROFILEFLAG|$coq_profile_flag|" \