* Adding compability with ocaml 3.10 + camlp5 (rework of

  the patch by S. Mimram)
* for detecting architecture, also look for /bin/uname
* restore the compatibility of kernel/byterun/coq_interp.c with 
  ocaml 3.07 (caml_modify vs. modify). There is still an issue 
  with this 3.07 and 64-bits architecture (see coqdev and a future 
  bug report). 




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

18 files changed, 144 insertions, 66 deletions

diff --git a/Makefile.build b/Makefile.build
index e814699f3..89ebaf6a1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -77,11 +77,9 @@ BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS=$(LOCALINCLUDES)
 
-OCAMLC_P4O=$(OCAMLC) -pp $(CAMLP4O) $(BYTEFLAGS)
-OCAMLOPT_P4O=$(OCAMLOPT) -pp $(CAMLP4O) $(OPTFLAGS)
 CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements 
 CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p'
-CAMLP4USE=sed -n -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p'
+CAMLP4USE=sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p'
 
 COQINCLUDES=          # coqtop includes itself the needed paths
 COQ_XML=	# is "-xml" when building XML library
@@ -707,12 +705,12 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto
 ## In other words, the Byte-only code doesn't import a new module.
 toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -DByte -impl $< > $@ \
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -DByte -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here 
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl $< > $@ \
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 # files compiled with -rectypes
@@ -804,7 +802,7 @@ endif
 
 %.ml4.preprocessed: %.ml4 | %.ml4.d
 	$(SHOW)'CAMLP4O $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
@@ -827,7 +825,7 @@ endif
 #Critical section:
 # Nobody (in a make -j) should touch the .ml file here.
 	$(SHOW)'OCAMLDEP4 $<'
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \
 	  || ( RV=$$?; rm -f "$*.ml"; exit $${RV} )
 	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml
diff --git a/config/Makefile.template b/config/Makefile.template
index 6161089ae..651985488 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -79,10 +79,6 @@ CAMLTIMEPROF=COQPROFILEFLAG
 # The best compiler: native (=opt) or bytecode (=byte) if no native compiler
 BEST=BESTCOMPILER
 
-# For Camlp4 use
-P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
-P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
-
 # Your architecture
 # Can be obtain by UNIX command arch
 ARCH=ARCHITECTURE
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 6882baa6f..54d92c62c 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -18,6 +18,7 @@ val coqtop : string     (* where are the sources *)
 val camldir : string    (* base directory of OCaml binaries *)
 val camllib : string    (* for Dynlink *)
 
+val camlp4 : string     (* exact name of camlp4: either "camlp4" ou "camlp5" *)
 val camlp4lib : string  (* where is the library of Camlp4 *)
 
 val best : string       (* byte/opt *)
diff --git a/configure b/configure
index 6d497e29f..41f057104 100755
--- a/configure
+++ b/configure
@@ -228,6 +228,8 @@ case $arch_spec in
 	    # cygwin returns a name of the form /cygdrive/c/... 
 	    # that coqc does not understand; need to transform it
 	    COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"`
+	elif test -x /bin/uname ; then
+	    ARCH=`/bin/uname -s`
 	elif test -x /usr/bin/uname ; then
 	    ARCH=`/usr/bin/uname -s`
 	else
@@ -359,17 +361,28 @@ fi
 
 CAMLLIB=`"$CAMLC" -where`
 
-# Camlp4 (greatly simplified since merged with ocaml)
+# Camlp4 / Camlp5 configuration
+# Very basic for the moment: if camlp5 exists, we use it...
 
+if [ -x "${CAMLLIB}/camlp5" ] ; then 
+    CAMLP4=camlp5
+    camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+else
+    case  $CAMLVERSION in 
+	3.10*)
+	    echo "Objective Caml 3.10 found but no Camlp5 installed"
+	    echo "Configuration script failed!"
+	    exit 1;;  
+	*) 
+	    CAMLP4=camlp4;;
+    esac
+fi
+CAMLP4LIB=+$CAMLP4
+FULLCAMLP4LIB=${CAMLLIB}/$CAMLP4
+# Assume that camlp(4|5) binaries are at the same place as ocaml ones
+# (this should become configurable some day) 
 CAMLP4BIN=${CAMLBIN}
 
-#case $OS in
-#  Win32)
-    CAMLP4LIB=+camlp4
-# ;;
-#  *)
-#    CAMLP4LIB=${CAMLLIB}/camlp4
-#esac
 
 # OS dependent libraries
 
@@ -612,13 +625,14 @@ escape_var () {
 EOF
 }
 
-export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB
+export COQTOP BINDIR LIBDIR CAMLBIN CAMLLIB CAMLP4 CAMLP4LIB FULLCAMLP4LIB
 ESCCOQTOP="`VAR=COQTOP escape_var`"
 ESCBINDIR="`VAR=BINDIR escape_var`"
 ESCLIBDIR="`VAR=LIBDIR escape_var`"
 ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
 ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
+ESCCAMLP4="`VAR=CAMLP4 escape_var`"
+ESCCAMLP4LIB="`VAR=FULLCAMLP4LIB escape_var`"
 
 mlconfig_file="$COQSRC/config/coq_config.ml"
 rm -f $mlconfig_file
@@ -631,6 +645,7 @@ let coqlib = "$ESCLIBDIR"
 let coqtop = "$ESCCOQTOP"
 let camldir = "$ESCCAMLDIR"
 let camllib = "$ESCCAMLLIB"
+let camlp4 = "$ESCCAMLP4"
 let camlp4lib = "$ESCCAMLP4LIB"
 let best = "$best_compiler"
 let arch = "$ARCH"
@@ -741,15 +756,10 @@ OCAMLDEBUGCOQ=$COQTOP/dev/ocamldebug-coq
 
 if test "$coq_debug_flag" = "-g" ; then
   rm -f $OCAMLDEBUGCOQ
-  if [ "$CAMLP4LIB" = "+camlp4" ] ; then
-    CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
-  else
-    CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
-  fi
   sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
       -e "s|COQLIBDIRECTORY|$LIBDIR|" \
       -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-      -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \
+      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
       $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
   chmod a-w,a+x $OCAMLDEBUGCOQ
 fi
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index d7c627248..45dee7831 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1350,8 +1350,8 @@ let build_clause eqs =
 	      (fun id -> ([],id),Tacexpr.InHyp)
 	      eqs
 	   );
-    onconcl = false; 
-    concl_occs = [] 
+    Tacexpr.onconcl = false; 
+    Tacexpr.concl_occs = [] 
   }
 
 let rec rewrite_eqs_in_eqs eqs = 
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 44680d6d6..2d1c62892 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -7,7 +7,11 @@ export COQLIB=COQLIBDIRECTORY
 export COQTH=$COQLIB/theories
 CAMLBIN=CAMLBINDIRECTORY
 OCAMLDEBUG=$CAMLBIN/ocamldebug
-export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+if [ -x "$CAMLBIN/camlp5" ]; then 
+  export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
+else
+  export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+fi
 
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ccfb2515a..0dd3b653a 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -80,6 +80,13 @@ sp is a local copy of the global variable extern_sp. */
 #   define print_int(i) 
 #endif
 
+/* Wrapper pour caml_modify */ 	 
+#ifdef OCAML_307 	 
+#define CAML_MODIFY(a,b) modify(a,b) 	 
+#else 	 
+#define CAML_MODIFY(a,b) caml_modify(a,b) 	 
+#endif
+
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
@@ -652,7 +659,7 @@ value coq_interprete
 	  Field(accu, 0) = sp[0];
 	  *sp = accu;
 	  /* mise a jour du block accumulate */
-	  caml_modify(&Field(p[i], 1),*sp);
+	  CAML_MODIFY(&Field(p[i], 1),*sp);
 	  sp++;
 	}
 	pc += nfunc;
@@ -823,7 +830,7 @@ value coq_interprete
       
       Instruct(SETFIELD0){
 	print_instr("SETFIELD0");
-	caml_modify(&Field(accu, 0),*sp);
+	CAML_MODIFY(&Field(accu, 0),*sp);
 	sp++;
 	Next;
       }
@@ -831,7 +838,7 @@ value coq_interprete
       Instruct(SETFIELD1){
         int i, j, size, size_aux;
 	print_instr("SETFIELD1");
-	caml_modify(&Field(accu, 1),*sp);
+	CAML_MODIFY(&Field(accu, 1),*sp);
        	sp++;
 	Next; 
       }
@@ -860,7 +867,7 @@ value coq_interprete
       
       Instruct(SETFIELD){
 	print_instr("SETFIELD");
-	caml_modify(&Field(accu, *pc),*sp);
+	CAML_MODIFY(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
       }	
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 6fe4c4c7e..40cffadb7 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -6,14 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_ifdef.cmo" i*)
+(*i camlp4use: "pa_macro.cmo" i*)
 
 (* Compatibility file depending on ocaml version *)
 
-(* IFDEF not available in 3.06; use ifdef instead *)
+IFDEF OCAML309 THEN DEFINE OCAML308 END
 
-(* type loc is different in 3.08 *)
-ifdef OCAML_308 then
+IFDEF CAMLP5 THEN 
+module M = struct 
+type loc = Stdpp.location
+let dummy_loc = Stdpp.dummy_loc
+let make_loc = Stdpp.make_loc
+let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else Stdpp.encl_loc loc1 loc2
+type token = string*string
+type lexer = token Token.glexer
+let using l x = l.Token.tok_using x
+end
+ELSE IFDEF OCAML308 THEN
 module M = struct
 type loc = Token.flocation
 let dummy_loc = Token.dummy_loc
@@ -26,16 +38,34 @@ let unloc (b,e) =
   assert (dummy_loc = (b,e) or make_loc loc = (b,e));
 *)
   loc
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2) 
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
 end
-else
+ELSE 
 module M = struct
 type loc = int * int
 let dummy_loc = (0,0)
 let make_loc x = x
 let unloc x = x
+let join_loc loc1 loc2 =
+ if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
+ else (fst loc1, snd loc2)
+type token = Token.t
+type lexer = Token.lexer
+let using l x = l.Token.using x
 end
+END
+END
 
 type loc = M.loc
 let dummy_loc = M.dummy_loc
-let unloc = M.unloc
 let make_loc = M.make_loc
+let unloc = M.unloc
+let join_loc = M.join_loc
+type token = M.token
+type lexer = M.lexer
+let using = M.using
diff --git a/lib/util.ml b/lib/util.ml
index 1d1c5e060..fa21cd83e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -26,15 +26,13 @@ type loc = Compat.loc
 let dummy_loc = Compat.dummy_loc
 let unloc = Compat.unloc
 let make_loc = Compat.make_loc
+let join_loc = Compat.join_loc
 
 (* raising located exceptions *)
 type 'a located = loc * 'a
 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)
-let join_loc loc1 loc2 =
-  if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
-  else (fst loc1, snd loc2)
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 7585ad4d8..b4fa39beb 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -14,7 +14,7 @@ open Genarg
 open Q_util
 open Q_coqast
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let join_loc = Util.join_loc
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
@@ -228,7 +228,7 @@ EXTEND
         let t, g = interp_entry_name loc e sep in (g, Some (s,t))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Pcoq.lexer.Token.using ("", s);
+	    Compat.using Pcoq.lexer ("", s);
         (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
     ] ]
   ;
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 8de2af4ec..e99741a6e 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -45,7 +45,7 @@ val extend_grammar : all_grammar_command -> unit
 type grammar_tactic_production =
   | TacTerm of string
   | TacNonTerm of
-      loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+      loc * (Compat.token Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
   string -> grammar_tactic_production list list -> unit
@@ -61,7 +61,7 @@ val get_extend_vernac_grammars :
 (*
 val reset_extend_grammars_v8 : unit -> unit
 *)
-val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol
+val interp_entry_name : int -> string -> entry_type * Compat.token Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 161a08bfa..b0e573eb9 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo" i*)
+(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
 (*i $Id$ i*)
 
@@ -31,6 +31,29 @@ open Ppextend
    we unfreeze the state of the lexer. This restores the behaviour of the
    lexer. B.B. *)
 
+IFDEF CAMLP5 THEN 
+
+let lexer = {
+  Token.tok_func = Lexer.func;
+  Token.tok_using = Lexer.add_token;
+  Token.tok_removing = (fun _ -> ());
+  Token.tok_match = Token.default_match;
+  (* Token.parse = Lexer.tparse; *)
+  Token.tok_comm = None;
+  Token.tok_text = Lexer.token_text }
+
+module L =
+  struct
+    type te = string * string
+    let lexer = lexer
+  end
+
+(* The parser of Coq *)
+
+module G = Grammar.GMake(L)
+
+ELSE 
+
 let lexer = {
   Token.func = Lexer.func;
   Token.using = Lexer.add_token;
@@ -47,6 +70,8 @@ module L =
 
 module G = Grammar.Make(L)
 
+END
+
 let grammar_delete e pos rls =
   List.iter
     (fun (n,ass,lev) ->
@@ -106,7 +131,7 @@ type ext_kind =
   | ByGrammar of
       grammar_object G.Entry.e * Gramext.position option *
       (string option * Gramext.g_assoc option *
-       (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+       (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
   | ByGEXTEND of (unit -> unit) * (unit -> unit)
 
 let camlp4_state = ref []
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 523ad92fb..f0d10dcb0 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -20,9 +20,9 @@ open Libnames
 
 (* The lexer and parser of Coq. *)
 
-val lexer : Token.lexer
+val lexer : Compat.lexer
 
-module Gram : Grammar.S with type te = Token.t
+module Gram : Grammar.S with type te = Compat.token
 
 (* The superclass of all grammar entries *)
 type grammar_object
@@ -42,7 +42,7 @@ val get_constr_entry :
 val grammar_extend :
   grammar_object Gram.Entry.e -> Gramext.position option ->
     (string option * Gramext.g_assoc option *
-     (Token.t Gramext.g_symbol list * Gramext.g_action) list) list
+     (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
 
 val remove_grammars : int -> unit
@@ -210,7 +210,7 @@ module Vernac_ :
 (* Binding entry names to campl4 entries *)
 
 val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
-  bool -> constr_production_entry -> Token.t Gramext.g_symbol
+  bool -> constr_production_entry -> Compat.token Gramext.g_symbol
 
 (* Registering/resetting the level of an entry *)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f5bab5d69..4b1dfd9e3 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "q_MLast.cmo pa_ifdef.cmo" i*)
+(*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
 
 (* $Id$ *)
 
@@ -21,13 +21,18 @@ let purge_str s =
   if String.length s == 0 || s.[0] <> '$' then s
   else String.sub s 1 (String.length s - 1)
 
+IFDEF OCAML308 THEN DEFINE NOP END
+IFDEF OCAML309 THEN DEFINE NOP END
+IFDEF CAMLP5 THEN DEFINE NOP END
+
 let anti loc x =
   let e =
     let loc =
-      ifdef OCAML_308 then
+      IFDEF NOP THEN 
         loc
-      else
-        (1, snd loc - fst loc)
+      ELSE 
+	(1, snd loc - fst loc)
+      END 
     in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 365435056..5d35298e8 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -32,7 +32,10 @@ let ide       = split_list Tolink.ide
 
 (* 3. Toplevel objects *)
 let camlp4topobjs =
-  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+  if Coq_config.camlp4 = "camlp5" then
+    ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+  else
+    ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
 let topobjs = camlp4topobjs
 
 let gramobjs = []
@@ -306,7 +309,7 @@ let main () =
     (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
     (* Now, with the .cma, we MUST use the -linkall option *)
-    let command = String.concat " " (prog::args) in
+    let command = String.concat " " (prog::"-rectypes"::args) in
     if !echo then 
       begin 
 	print_endline command; 
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index cc3b60923..02bfbbb37 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -175,7 +175,8 @@ let variables l =
     | _ :: r -> var_aux r
   in
   section "Variables definitions.";
-  print "CAMLP4LIB=`camlp4 -where`\n";
+  print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n";
+  print "CAMLP4=`basename $CAMLP4LIB`\n"; 
 (*  print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
   print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
   -I $(COQTOP)/library -I $(COQTOP)/parsing \\
@@ -204,8 +205,8 @@ let variables l =
   print "CAMLOPTLINK=ocamlopt\n";
   print "COQDEP=$(COQBIN)coqdep -c\n";
   print "GRAMMARS=grammar.cma\n";
-  print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n";
-  print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
+  print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+  print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
   var_aux l;
   print "\n"
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 855c98f93..9a162997b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -28,7 +28,7 @@ open Notation
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+let cache_token (_,s) = Compat.using Pcoq.lexer ("", s)
 
 let (inToken, outToken) =
   declare_object {(default_object "TOKEN") with
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index c0e090290..43ab05aa8 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_ifdef.cmo" i*)
+(*i camlp4use: "pa_macro.cmo" i*)
 (* WARNING
  * camlp4deps will not work for this file unless Makefile system enhanced.
  *)
@@ -103,7 +103,7 @@ let dir_ml_load s =
                 str s; str" to Coq code." >])
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      ifdef Byte then
+      IFDEF Byte THEN
 	(* WARNING
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
@@ -117,7 +117,7 @@ let dir_ml_load s =
 	    [Filename.dirname gname]
 	with | Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
-      else ()
+      ELSE () END
     | Native ->
 	errorlabstrm "Mltop.no_load_object"
           [< str"Loading of ML object file forbidden in a native Coq" >]