Mise en place mécanisme de compatibilité ocaml 3.08

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

4 files changed, 39 insertions, 21 deletions

diff --git a/Makefile b/Makefile
index 949d03dbb..e688304e3 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,7 @@
 
 include config/Makefile
 
-noargument:
+NOARG:
 	@echo "Please use either"
 	@echo "   ./configure"
 	@echo "   make world"
@@ -84,7 +84,7 @@ DEPFLAGS=$(LOCALINCLUDES)
 
 OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
-CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo q_MLast.cmo
+CAMLP4EXTENDFLAGS=-I . pa_extend.cmo pa_extend_m.cmo pa_macro.cmo q_MLast.cmo
 CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p'
 
 COQINCLUDES=          # coqtop includes itself the needed paths
@@ -107,7 +107,7 @@ CONFIG=\
   config/coq_config.cmo
 
 LIBREP=\
-  lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/bignat.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bignat.cmo \
   lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
   lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
   lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
@@ -1297,7 +1297,7 @@ ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \
             parsing/g_prim.ml4 parsing/pcoq.ml4
 
 GRAMMARNEEDEDCMO=\
-  lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/bignat.cmo \
+  lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bignat.cmo \
   lib/dyn.cmo lib/options.cmo \
   lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \
   kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \
@@ -1396,9 +1396,20 @@ proofs/tacexpr.cmx: proofs/tacexpr.ml
 	$(SHOW)'OCAMLOPT  -rectypes $<'
 	$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $<
 
+# files compiled with camlp4 because of macros
+
+lib/compat.cmo: lib/compat.ml4
+	$(SHOW)'OCAMLC4  $<' 
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $<
+
+lib/compat.cmx: lib/compat.ml4
+	$(SHOW)'OCAMLC  $<' 
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $<
+
 # files compiled with camlp4 because of streams syntax
 
 ML4FILES += lib/pp.ml4 			\
+	 lib/compat.ml4 		\
 	 contrib/xml/xml.ml4		\
 	 contrib/xml/acic2Xml.ml4	\
 	 contrib/xml/proofTree2Xml.ml4	\
diff --git a/lib/compat.ml4 b/lib/compat.ml4
new file mode 100644
index 000000000..57c7915e3
--- /dev/null
+++ b/lib/compat.ml4
@@ -0,0 +1 @@
+type loc = int * int let dummy_loc = 0, 0 let unloc x = x let make_loc x = x
diff --git a/lib/util.ml b/lib/util.ml
index 9c51f3968..1aa3786f2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
@@ -22,10 +22,13 @@ let errorlabstrm l pps = raise (UserError(l,pps))
 
 let todo s = prerr_string ("TODO: "^s^"\n")
 
+type loc = Compat.loc
+let dummy_loc = Compat.dummy_loc
+let unloc = Compat.unloc
+let make_loc = Compat.make_loc
+
 (* raising located exceptions *)
-type loc = int * int
 type 'a located = loc * 'a
-let dummy_loc = (0,0)
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
diff --git a/lib/util.mli b/lib/util.mli
index 79133a930..45e953a64 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
@@ -32,9 +32,12 @@ val errorlabstrm : string -> std_ppcmds -> 'a
 
 val todo : string -> unit
 
-type loc = int * int
+type loc = Compat.loc
+
 type 'a located = loc * 'a
 
+val unloc : loc -> int * int
+val make_loc : int * int -> loc
 val dummy_loc : loc
 val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a