New upstream release.debian/8.1.pl2+dfsg-1

7 files changed, 24 insertions, 584 deletions

diff --git a/debian/changelog b/debian/changelog
index 527e5c78..3bb3c0a4 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,8 +1,12 @@
-coq (8.1.pl1+dfsg-4) UNRELEASED; urgency=low
+coq (8.1.pl2+dfsg-1) experimental; urgency=low
 
+  * New upstream release.
+  * Removed camlp5.dpatch, integrated upstream.
+  * Updated browser.dpatch, coqdoc_stdlib.dpatch and makefile.dpatch.
   * Corrected emacs-mode startup file, closes: #446170.
+  * Removed Sven Luther from uploaders.
 
- -- Samuel Mimram <smimram@debian.org>  Wed, 10 Oct 2007 22:36:07 +0000
+ -- Samuel Mimram <smimram@debian.org>  Mon, 15 Oct 2007 18:55:09 +0000
 
 coq (8.1.pl1+dfsg-3) unstable; urgency=low
 
diff --git a/debian/control b/debian/control
index 3824703e..338fb38a 100644
--- a/debian/control
+++ b/debian/control
@@ -2,7 +2,7 @@ Source: coq
 Section: math
 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>
+Uploaders: Ralf Treinen <treinen@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.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
diff --git a/debian/patches/00list b/debian/patches/00list
index 333bbd2f..bbb91a76 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +1,3 @@
-camlp5
 coqdoc_stdlib
 browser
 makefile
diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch
index ba55f3de..9a15372c 100755
--- a/debian/patches/browser.dpatch
+++ b/debian/patches/browser.dpatch
@@ -5,15 +5,15 @@
 ## DP: Use the default Debian browser for help.
 
 @DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml
---- coq-8.0pl3+8.1alpha~/lib/options.ml	2005-12-26 20:07:21.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/lib/options.ml	2006-04-29 16:06:20.000000000 +0000
-@@ -117,7 +117,4 @@
+diff -urNad coq-8.1.pl2+dfsg~/lib/options.ml coq-8.1.pl2+dfsg/lib/options.ml
+--- coq-8.1.pl2+dfsg~/lib/options.ml	2007-10-15 11:00:52.000000000 +0000
++++ coq-8.1.pl2+dfsg/lib/options.ml	2007-10-15 11:01:51.000000000 +0000
+@@ -118,7 +118,4 @@
             "\" must contain exactly one placeholder \"%s\".")
     else pre,post
   with
 -  Not_found ->
 -   if Sys.os_type = "Win32"
 -   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
--   else "netscape -remote \"OpenURL(", ")\""
+-   else "firefox -remote \"OpenURL(", ")\""
 +  Not_found -> "/usr/bin/x-www-browser ", ""
diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch
deleted file mode 100755
index 2c5b8643..00000000
--- a/debian/patches/camlp5.dpatch
+++ /dev/null
@@ -1,563 +0,0 @@
-#! /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
diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
index fb618f56..f59f52e0 100755
--- a/debian/patches/coqdoc_stdlib.dpatch
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -6,14 +6,14 @@
 ## DP: to be able to build the documentation before coqdoc is installed.
 
 @DPATCH@
-diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile
---- coq-8.0pl3+8.1beta~/doc/Makefile	2006-06-16 13:02:33.000000000 +0000
-+++ coq-8.0pl3+8.1beta/doc/Makefile	2006-06-16 13:19:11.000000000 +0000
-@@ -216,6 +216,7 @@
+diff -urNad coq-8.1.pl2+dfsg~/doc/Makefile coq-8.1.pl2+dfsg/doc/Makefile
+--- coq-8.1.pl2+dfsg~/doc/Makefile	2007-10-15 11:45:13.000000000 +0000
++++ coq-8.1.pl2+dfsg/doc/Makefile	2007-10-15 11:45:40.000000000 +0000
+@@ -222,6 +222,7 @@
  	mkdir stdlib/html
  	(cd stdlib/html;\
  	 $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\
-+	  --coqlib_path $(COQTOP) \
- 	  -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v)
++	 --coqlib_path $(COQSRC) \
+ 	  -R $(COQSRC)/theories Coq $(COQSRC)/theories/*/*.v)
  	mv stdlib/html/index.html stdlib/index-body.html
  
diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch
index b656a9bb..d16030ca 100755
--- a/debian/patches/makefile.dpatch
+++ b/debian/patches/makefile.dpatch
@@ -6,15 +6,15 @@
 ## DP: when compiling on non-native archs.
 
 @DPATCH@
-diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile
---- coq-8.0pl3+8.1alpha~/Makefile	2006-04-07 15:08:12.000000000 +0000
-+++ coq-8.0pl3+8.1alpha/Makefile	2006-04-30 11:41:09.000000000 +0000
-@@ -1401,7 +1401,7 @@
+diff -urNad coq-8.1.pl2+dfsg~/Makefile coq-8.1.pl2+dfsg/Makefile
+--- coq-8.1.pl2+dfsg~/Makefile	2007-10-15 11:02:54.000000000 +0000
++++ coq-8.1.pl2+dfsg/Makefile	2007-10-15 11:03:55.000000000 +0000
+@@ -1479,7 +1479,7 @@
  parsing/grammar.cma: $(GRAMMARCMO)
  	$(SHOW)'Testing $@'
  	@touch test.ml4
--	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
-+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
+-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
++	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
  	@rm -f test-grammar test.*
  	$(SHOW)'OCAMLC -a $@'   
  	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@