Preliminary patch for OCaml 3.10.

4 files changed, 530 insertions, 1 deletions

diff --git a/debian/changelog b/debian/changelog
index 84b48e29..7d341668 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,11 @@
+coq (8.1.pl1+dfsg-2) experimental; urgency=low
+
+  * Updated for OCaml 3.10.
+  * Build-depend on camlp5.
+  * Added camlp5.dpatch to fix compilation problems.
+
+ -- Samuel Mimram <smimram@debian.org>  Wed, 22 Aug 2007 16:39:04 +0000
+
 coq (8.1.pl1+dfsg-1) unstable; urgency=low
 
   * New upstream release.
diff --git a/debian/control b/debian/control
index 291549c2..7c473bf4 100644
--- a/debian/control
+++ b/debian/control
@@ -4,7 +4,7 @@ Priority: optional
 Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
 Uploaders: Ralf Treinen <treinen@debian.org>, Sven Luther <luther@debian.org>, Remi Vanicat <vanicat@debian.org>, Stefano Zacchiroli <zack@debian.org>, Samuel Mimram <smimram@debian.org>
 Standards-Version: 3.7.2
-Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), texlive-latex-extra, hevea
+Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.10), ocaml-best-compilers, camlp5, liblablgtk2-ocaml-dev (>= 2.4.0), texlive-latex-extra, hevea
 XS-Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/coq
 XS-Vcs-Browser: http://svn.debian.org/wsvn/pkg-ocaml-maint/trunk/packages/coq/trunk/
 
diff --git a/debian/patches/00list b/debian/patches/00list
index bbb91a76..333bbd2f 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,3 +1,4 @@
+camlp5
 coqdoc_stdlib
 browser
 makefile
diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch
new file mode 100755
index 00000000..9de2b6a7
--- /dev/null
+++ b/debian/patches/camlp5.dpatch
@@ -0,0 +1,520 @@
+#! /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: No description.
+
+@DPATCH@
+diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile
+--- coq-8.1.pl1+dfsg~/Makefile	2007-08-22 16:33:31.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile	2007-08-22 16:36:36.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/Makefile.dep	2007-08-22 16:36:36.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/config/Makefile.template	2007-08-22 16:36:36.000000000 +0000
+@@ -62,7 +62,7 @@
+ CAMLMKTOP="CAMLMKTOPEXEC"
+ 
+ # Caml flags
+-CAMLFLAGS=CAMLANNOTATEFLAG
++CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
+ 
+ # Compilation debug flag
+ CAMLDEBUG=COQDEBUGFLAG
+diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure
+--- coq-8.1.pl1+dfsg~/configure	2007-08-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/configure	2007-08-22 16:36:36.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~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4
+--- coq-8.1.pl1+dfsg~/lib/compat.ml4	2007-08-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/compat.ml4	2007-08-22 16:36:36.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/lib/util.ml	2007-08-22 16:36:36.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/argextend.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/egrammar.mli	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/pcoq.mli	2007-08-22 16:36:36.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/q_util.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml	2007-08-22 16:36:45.000000000 +0000
+@@ -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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4	2007-08-22 16:36:36.000000000 +0000
+@@ -204,7 +204,7 @@
+   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 "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+   print "PP=-pp \"camlp4o -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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4	2007-08-22 16:36:45.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-22 16:33:10.000000000 +0000
++++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml	2007-08-22 16:36:45.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