#! /bin/sh /usr/share/dpatch/dpatch-run
## camlp5.dpatch by Samuel Mimram <smimram@debian.org>
##
## All lines beginning with `## DP:' are a description of the patch.
## DP: Use camlp5 instead of the new camlp4 for coq.

@DPATCH@
diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile
--- coq-8.1.pl1+dfsg~/Makefile	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/Makefile	2007-08-24 10:56:52.000000000 +0000
@@ -1504,11 +1504,11 @@
 
 # BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml
 
-# File using pa_ifdef and only necessary for parsing ml files
+# File using pa_macro and only necessary for parsing ml files
 
 parsing/q_coqast.cmo: parsing/q_coqast.ml4
 	$(SHOW)'OCAMLC4  $<' 
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo $(CAMLP4COMPAT) -impl" -c -impl $<
 
 # toplevel/mltop.ml4 (ifdef Byte)
 
@@ -1522,11 +1522,11 @@
 
 toplevel/mltop.byteml: toplevel/mltop.ml4
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@
 
 toplevel/mltop.optml: toplevel/mltop.ml4
 	$(SHOW)'CAMLP4O   $<'	
-	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@
+	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -impl $< > $@ || rm -f $@
 
 ML4FILES += toplevel/mltop.ml4
 
@@ -1571,11 +1571,11 @@
 
 lib/compat.cmo: lib/compat.ml4
 	$(SHOW)'OCAMLC4  $<' 
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $<
 
 lib/compat.cmx: lib/compat.ml4
 	$(SHOW)'OCAMLOPT  $<' 
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $<
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $<
 
 # files compiled with camlp4 because of streams syntax
 
@@ -1654,7 +1654,7 @@
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $<
 
 %.ml: %.ml4
-	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
 
 #.v.vo:
 #	$(BOOTCOQTOP) -compile $*
diff -urNad coq-8.1.pl1+dfsg~/Makefile.dep coq-8.1.pl1+dfsg/Makefile.dep
--- coq-8.1.pl1+dfsg~/Makefile.dep	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/Makefile.dep	2007-08-24 10:56:52.000000000 +0000
@@ -12,4 +12,4 @@
 include .depend.camlp4
 
 .ml4.ml:
-	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
+	$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@
diff -urNad coq-8.1.pl1+dfsg~/config/Makefile.template coq-8.1.pl1+dfsg/config/Makefile.template
--- coq-8.1.pl1+dfsg~/config/Makefile.template	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/config/Makefile.template	2007-08-24 10:56:52.000000000 +0000
@@ -62,7 +62,7 @@
 CAMLMKTOP="CAMLMKTOPEXEC"
 
 # Caml flags
-CAMLFLAGS=CAMLANNOTATEFLAG
+CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
 
 # Compilation debug flag
 CAMLDEBUG=COQDEBUGFLAG
@@ -80,8 +80,8 @@
 BEST=BESTCOMPILER
 
 # For Camlp4 use
-P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing
-P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
+P4=$(COQTOP)/bin/$(ARCH)/call_camlp5 -I $(COQTOP)/src/parsing
+P4DEP=$(COQTOP)/bin/$(ARCH)/camlp5dep
 
 # Your architecture
 # Can be obtain by UNIX command arch
diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure
--- coq-8.1.pl1+dfsg~/configure	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/configure	2007-08-24 10:56:52.000000000 +0000
@@ -78,7 +78,7 @@
 ocamllexexec=ocamllex
 ocamlyaccexec=ocamlyacc
 ocamlmktopexec=ocamlmktop
-camlp4oexec=camlp4o
+camlp4oexec=camlp5o
 
 
 coq_debug_flag=
@@ -153,7 +153,7 @@
                   arch=$2
 		  shift;;
     -opt|--opt) bytecamlc=ocamlc.opt
-                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
+                camlp4oexec=camlp5o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
     -fsets|--fsets) fsets_opt=yes
                     case "$2" in
@@ -297,7 +297,7 @@
 	 ocamllexexec=$CAMLBIN/ocamllex
 	 ocamlyaccexec=$CAMLBIN/ocamlyacc
 	 camlmktopexec=$CAMLBIN/ocamlmktop
-	 camlp4oexec=$CAMLBIN/camlp4o
+	 camlp4oexec=$CAMLBIN/camlp5o
 esac
 
 if test ! -f "$CAMLC" ; then
@@ -362,10 +362,10 @@
 
 #case $OS in
 #  Win32)
-    CAMLP4LIB=+camlp4
+    CAMLP4LIB=+camlp5
 # ;;
 #  *)
-#    CAMLP4LIB=${CAMLLIB}/camlp4
+#    CAMLP4LIB=${CAMLLIB}/camlp5
 #esac
 
 # OS dependent libraries
@@ -615,7 +615,7 @@
 ESCLIBDIR="`VAR=LIBDIR escape_var`"
 ESCCAMLDIR="`VAR=CAMLBIN escape_var`"
 ESCCAMLLIB="`VAR=CAMLLIB escape_var`"
-ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4
+ESCCAMLP4LIB="$ESCCAMLLIB"/camlp5
 
 mlconfig_file="$COQSRC/config/coq_config.ml"
 rm -f $mlconfig_file
@@ -739,8 +739,8 @@
 
 if test "$coq_debug_flag" = "-g" ; then
   rm -f $OCAMLDEBUGCOQ
-  if [ "$CAMLP4LIB" = "+camlp4" ] ; then
-    CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4
+  if [ "$CAMLP4LIB" = "+camlp5" ] ; then
+    CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp5
   else
     CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB
   fi
diff -urNad coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template
--- coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template	2007-08-24 10:56:52.000000000 +0000
@@ -7,7 +7,7 @@
 export COQTH=$COQLIB/theories
 CAMLBIN=CAMLBINDIRECTORY
 OCAMLDEBUG=$CAMLBIN/ocamldebug
-export CAMLP4LIB=`$CAMLBIN/camlp4 -where`
+export CAMLP4LIB=`$CAMLBIN/camlp5 -where`
 
 exec $OCAMLDEBUG \
 	-I $CAMLP4LIB \
diff -urNad coq-8.1.pl1+dfsg~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4
--- coq-8.1.pl1+dfsg~/lib/compat.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/lib/compat.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -11,6 +11,7 @@
 (* IFDEF not available in 3.06; use ifdef instead *)
 
 (* type loc is different in 3.08 *)
+(*
 ifdef OCAML_308 then
 module M = struct
 type loc = Token.flocation
@@ -32,8 +33,9 @@
 let make_loc x = x
 let unloc x = x
 end
+*)
 
-type loc = M.loc
-let dummy_loc = M.dummy_loc
-let unloc = M.unloc
-let make_loc = M.make_loc
+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
diff -urNad coq-8.1.pl1+dfsg~/lib/util.ml coq-8.1.pl1+dfsg/lib/util.ml
--- coq-8.1.pl1+dfsg~/lib/util.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/lib/util.ml	2007-08-24 10:56:52.000000000 +0000
@@ -34,7 +34,7 @@
 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)
+  else Stdpp.encl_loc loc1 loc2
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
diff -urNad coq-8.1.pl1+dfsg~/parsing/argextend.ml4 coq-8.1.pl1+dfsg/parsing/argextend.ml4
--- coq-8.1.pl1+dfsg~/parsing/argextend.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/argextend.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -12,7 +12,7 @@
 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 >>
 
@@ -226,7 +226,7 @@
         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);
+	    Pcoq.lexer.Token.tok_using ("", s);
         (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None)
     ] ]
   ;
diff -urNad coq-8.1.pl1+dfsg~/parsing/egrammar.mli coq-8.1.pl1+dfsg/parsing/egrammar.mli
--- coq-8.1.pl1+dfsg~/parsing/egrammar.mli	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/egrammar.mli	2007-08-24 10:56:52.000000000 +0000
@@ -45,7 +45,7 @@
 type grammar_tactic_production =
   | TacTerm of string
   | TacNonTerm of
-      loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option
+      loc * ((string * string) Gramext.g_symbol * Genarg.argument_type) * string option
 
 val extend_tactic_grammar :
   string -> grammar_tactic_production list list -> unit
@@ -61,7 +61,7 @@
 (*
 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 * (string * string) Gramext.g_symbol
 
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) -> notation_grammar
diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 coq-8.1.pl1+dfsg/parsing/pcoq.ml4
--- coq-8.1.pl1+dfsg~/parsing/pcoq.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -30,20 +30,23 @@
    lexer. B.B. *)
 
 let lexer = {
-  Token.func = Lexer.func;
-  Token.using = Lexer.add_token;
-  Token.removing = (fun _ -> ());
-  Token.tparse = Lexer.tparse;
-  Token.text = Lexer.token_text }
+  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.Make(L)
+module G = Grammar.GMake(L)
 
 let grammar_delete e rls =
   List.iter
@@ -95,7 +98,7 @@
   | 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
+       ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list
   | ByGEXTEND of (unit -> unit) * (unit -> unit)
 
 let camlp4_state = ref []
diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.mli coq-8.1.pl1+dfsg/parsing/pcoq.mli
--- coq-8.1.pl1+dfsg~/parsing/pcoq.mli	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/pcoq.mli	2007-08-24 10:56:52.000000000 +0000
@@ -20,9 +20,9 @@
 
 (* The lexer and parser of Coq. *)
 
-val lexer : Token.lexer
+val lexer : (string * string) Token.glexer
 
-module Gram : Grammar.S with type te = Token.t
+module Gram : Grammar.S with type te = (string * string)
 
 (* The superclass of all grammar entries *)
 type grammar_object
@@ -42,7 +42,7 @@
 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
+     ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list
     -> unit
 
 val remove_grammars : int -> unit
@@ -210,7 +210,7 @@
 (* 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 -> (string * string) Gramext.g_symbol
 
 (* Registering/resetting the level of an entry *)
 
diff -urNad coq-8.1.pl1+dfsg~/parsing/ppconstr.ml coq-8.1.pl1+dfsg/parsing/ppconstr.ml
--- coq-8.1.pl1+dfsg~/parsing/ppconstr.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml	2007-08-24 10:56:52.000000000 +0000
@@ -95,9 +95,9 @@
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let pr_located pr ((b,e),x) =
-  if Options.do_translate() && (b,e)<>dummy_loc then
-    let (b,e) = unloc (b,e) in
+let pr_located pr (loc,x) =
+  if Options.do_translate() && loc<>dummy_loc then
+    let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
 
@@ -142,7 +142,7 @@
   | CHole _ -> mt ()
   | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
diff -urNad coq-8.1.pl1+dfsg~/parsing/ppvernac.ml coq-8.1.pl1+dfsg/parsing/ppvernac.ml
--- coq-8.1.pl1+dfsg~/parsing/ppvernac.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml	2007-08-24 10:56:52.000000000 +0000
@@ -28,7 +28,7 @@
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
@@ -39,7 +39,7 @@
 
 let pr_fqid fqid = str (string_of_fqid fqid)
 
-let pr_lfqid (_,_ as loc,fqid) =
+let pr_lfqid (loc,fqid) =
   if loc <> dummy_loc then
    let (b,_) = unloc loc in
     pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
diff -urNad coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 coq-8.1.pl1+dfsg/parsing/q_coqast.ml4
--- coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -22,10 +22,8 @@
 let anti loc x =
   let e =
     let loc =
-      ifdef OCAML_308 then
-        loc
-      else
-        (1, snd loc - fst loc)
+      loc
+      (* (1, snd loc - fst loc) *)
     in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
diff -urNad coq-8.1.pl1+dfsg~/parsing/q_util.ml4 coq-8.1.pl1+dfsg/parsing/q_util.ml4
--- coq-8.1.pl1+dfsg~/parsing/q_util.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/q_util.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -37,18 +37,18 @@
   List.fold_right
     (fun e1 e2 ->
       let e1 = f e1 in
-       let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+       let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
        <:expr< [$e1$ :: $e2$] >>)
     l (let loc = dummy_loc in <:expr< [] >>)
 
 let mlexpr_of_pair m1 m2 (a1,a2) =
   let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
   <:expr< ($e1$, $e2$) >>
 
 let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
   let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
   <:expr< ($e1$, $e2$, $e3$) >>
 
 (* We don't give location for tactic quotation! *)
diff -urNad coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 coq-8.1.pl1+dfsg/parsing/tacextend.ml4
--- coq-8.1.pl1+dfsg~/parsing/tacextend.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -13,7 +13,7 @@
 open Q_coqast
 open Argextend
 
-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 >>
 
diff -urNad coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 coq-8.1.pl1+dfsg/parsing/vernacextend.ml4
--- coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -13,7 +13,7 @@
 open Q_coqast
 open Argextend
 
-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 >>
 
diff -urNad coq-8.1.pl1+dfsg~/scripts/coqmktop.ml coq-8.1.pl1+dfsg/scripts/coqmktop.ml
--- coq-8.1.pl1+dfsg~/scripts/coqmktop.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml	2007-08-24 10:57:13.000000000 +0000
@@ -32,7 +32,7 @@
 
 (* 3. Toplevel objects *)
 let camlp4topobjs =
-  ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+  ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
 let topobjs = camlp4topobjs
 
 let gramobjs = []
@@ -285,12 +285,12 @@
 	(* native code *)
 	if !top then failwith "no custom toplevel in native code !";
 	let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in
-          (if !caml_inline_0 then ocamloptexec^" -linkall"^" -inline 0" else ocamloptexec^" -linkall")
+          (if !caml_inline_0 then ocamloptexec^" -linkall -rectypes"^" -inline 0" else ocamloptexec^" -linkall -rectypes")
       end else
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
       let ocamlmktoplib = " toplevellib.cma" in
       let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
-      let ocamlccustom = ocamlcexec^" -custom -linkall" in
+      let ocamlccustom = ocamlcexec^" -custom -linkall -rectypes" in
 	(if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
   in
     (* files to link *)
diff -urNad coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 coq-8.1.pl1+dfsg/tools/coq_makefile.ml4
--- coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -175,7 +175,7 @@
     | _ :: r -> var_aux r
   in
   section "Variables definitions.";
-  print "CAMLP4LIB=`camlp4 -where`\n";
+  print "CAMLP4LIB=`camlp5 -where`\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 +204,8 @@
   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 \"camlp5o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
   var_aux l;
   print "\n"
 
diff -urNad coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml coq-8.1.pl1+dfsg/toplevel/metasyntax.ml
--- coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml	2007-08-24 10:56:52.000000000 +0000
@@ -28,7 +28,7 @@
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
+let cache_token (_,s) = Pcoq.lexer.Token.tok_using ("", s)
 
 let (inToken, outToken) =
   declare_object {(default_object "TOKEN") with
diff -urNad coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 coq-8.1.pl1+dfsg/toplevel/mltop.ml4
--- coq-8.1.pl1+dfsg~/toplevel/mltop.ml4	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4	2007-08-24 10:56:52.000000000 +0000
@@ -98,7 +98,7 @@
                 str s; str" to Coq code." >])
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
-      ifdef Byte then
+      IFDEF Byte THEN
         let _,gname = where_in_path !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
@@ -108,7 +108,7 @@
 	    [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" >]
diff -urNad coq-8.1.pl1+dfsg~/toplevel/toplevel.ml coq-8.1.pl1+dfsg/toplevel/toplevel.ml
--- coq-8.1.pl1+dfsg~/toplevel/toplevel.ml	2007-08-24 10:56:51.000000000 +0000
+++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml	2007-08-24 10:56:52.000000000 +0000
@@ -139,16 +139,16 @@
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s inlibrary fname (bp,ep) =
+let print_location_in_file s inlibrary fname loc =
   let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
-  if (bp,ep) = dummy_loc then 
+  if loc = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     if inlibrary then
       (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
-       str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+       str" characters " ++ Cerrors.print_loc loc ++ fnl ())
     else
-    let (bp,ep) = unloc (bp,ep) in
+    let (bp,ep) = unloc loc in
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -172,15 +172,16 @@
            str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
     | None -> (mt ())
 
-let valid_loc dloc (b,e) =
-  (b,e) <> dummy_loc
+let valid_loc dloc loc =
+  let b, e = unloc loc in
+  loc <> dummy_loc
   & match dloc with
-    | Some (bd,ed) -> bd<=b & e<=ed
+    | Some dloc -> let bd,ed = unloc dloc in bd<=b & e<=ed
     | _ -> true
 	  
-let valid_buffer_loc ib dloc (b,e) =
-  valid_loc dloc (b,e) & 
-  let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
+let valid_buffer_loc ib dloc loc =
+  valid_loc dloc loc & 
+  let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing