18 files changed, 285 insertions, 614 deletions

diff --git a/debian/changelog b/debian/changelog
index afb42a67..a161de61 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,96 @@
+coq (8.1+dfsg-2) experimental; urgency=low
+
+  * Added cmxa-install.dpatch to install cmxa only on native archs,
+    closes: #415867.
+  * Added configure.dpatch for the configure to correctly detect whether
+    ocamlopt is present or not.
+  * Use dh_installtex instead of hand-crafted postinst.
+
+ -- Samuel Mimram <smimram@debian.org>  Sun, 18 Mar 2007 13:21:56 +0100
+
+coq (8.1+dfsg-1) experimental; urgency=low
+
+  * New upstream release.
+  * Removed system.dpatch and next-ia64.dpatch, integrated upstream.
+  * Removed the subdirectories common, faq, RecTutorial, refman, rt, tools,
+    tutorial of the directory doc since they contain documentation under the
+    Open Publication License which is not DFSG-free (thus the +dfsg in the
+    version number). The script debian/utils/purify_tarball automates this
+    process. This documentation in packaged separately in non-free, in
+    the coq-doc package.
+
+ -- Samuel Mimram <smimram@debian.org>  Tue, 13 Feb 2007 11:38:43 +0000
+
+coq (8.1~gamma-4) experimental; urgency=low
+
+  * Correctly build glob.dump on non-native archs, closes: #400535.
+
+ -- Samuel Mimram <smimram@debian.org>  Sun, 11 Feb 2007 18:02:49 +0100
+
+coq (8.1~gamma-3) experimental; urgency=low
+
+  * Added next-ia64.dpatch to fix the FTBFS on ia64.
+  * Correctly install coqdoc.sty, closes: #409027.
+  * Build-depend on tetex-extra | texlive-latex-extra in order to allow
+    building with texlive.
+
+ -- Samuel Mimram <smimram@debian.org>  Sun,  4 Feb 2007 20:38:43 +0100
+
+coq (8.1~gamma-2) experimental; urgency=low
+
+  * Added no-complexity-test.dpatch to skip complexity checks (thanks Julien
+    Cristau), closes: #399919.
+
+ -- Samuel Mimram <smimram@debian.org>  Thu, 23 Nov 2006 14:27:15 +0000
+
+coq (8.1~gamma-1) experimental; urgency=low
+
+  * New upstream release.
+  * Made the package binNMU-safe.
+  * Minor improvements of the coqide.desktop file, closes: #383310.
+  * Added system.dpatch to avoid erroneous interpretation of ~.
+  * Removed assert.dpatch, integrated upstream.
+
+ -- Samuel Mimram <smimram@debian.org>  Tue, 21 Nov 2006 13:33:55 +0000
+
+coq (8.0pl3+8.1beta.2-1) experimental; urgency=low
+
+  * New upstream beta release.
+  * Added assert.dpatch to check assertions in native mode.
+
+ -- Samuel Mimram <smimram@debian.org>  Thu, 13 Jul 2006 16:28:24 +0000
+
+coq (8.0pl3+8.1beta-1) experimental; urgency=low
+
+  * New upstream release.
+  * Added --fsets all option to configure to build the theory of finite sets. 
+  * Updated coqdoc_stdlib.dpatch, partly integrated upstream.
+  * Removed failing_tests.dpath, all the tests should succeed now.
+  * We don't need to remove rpaths anymore.
+  * Updated standards version to 3.7.2, no changes needed.
+
+ -- Samuel Mimram <smimram@debian.org>  Fri, 16 Jun 2006 12:59:07 +0000
+
+coq (8.0pl3+8.1alpha-2) experimental; urgency=low
+
+  * Added makefile.dpatch in order for ocamlopt not to be called when
+    compiling on non-native archs.
+  * Do not build the pdf documentation for the library since we don't ship it.
+    This will avoid the FTBFS because of missing LaTeX fonts.
+
+ -- Samuel Mimram <smimram@debian.org>  Sun, 30 Apr 2006 11:51:57 +0000
+
+coq (8.0pl3+8.1alpha-1) experimental; urgency=low
+
+  * New upstream release.
+  * No longer providing the compatibility coq7-libs package.
+  * coq-libs is now providing its documentation in html format.
+  * Added browser.dpatch to use the default Debian browser for help.
+  * Disabling checks which don't succeed for now: failing_tests.dpatch.
+  * Removed coq-8.0pl3-ocaml-3.09.dpatch.
+
+ -- Samuel Mimram <smimram@debian.org>  Thu, 27 Apr 2006 13:43:16 +0000
+
 coq (8.0pl3-2) unstable; urgency=low
 
   * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from
diff --git a/debian/control b/debian/control
index 92b0d596..88c3e39b 100644
--- a/debian/control
+++ b/debian/control
@@ -3,16 +3,16 @@ 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>
-Standards-Version: 3.6.2
-Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath
+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), tetex-extra | 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/
 
 Package: coq
 Architecture: any
-Depends: ${shlibs:Depends}, coq-libs (= ${Source-Version})
+Depends: ${shlibs:Depends}, ${misc:Depends}, coq-libs (= ${source:Version})
 Recommends: coqide | proofgeneral-coq
-Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle
+Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle, coq-doc
 Description: proof assistant for higher-order logic (toplevel and compiler)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
@@ -41,7 +41,7 @@ Description: proof assistant for higher-order logic (gtk interface)
 Package: coq-libs
 Architecture: all
 Recommends: coq (>= 8.0)
-Conflicts: coq (<< 8.0)
+Conflicts: coq (<< 8.0), coq-doc (<= 8.0pl1.0-2)
 Description: proof assistant for higher-order logic (theories)
  Coq is a proof assistant for higher-order logic, which allows the
  development of computer programs consistent with their formal
@@ -50,18 +50,3 @@ Description: proof assistant for higher-order logic (theories)
  .
  This package provides existing theories that new proofs can be
  based upon, including theories of arithmetic and Boolean values.
-
-Package: coq7-libs
-Architecture: all
-Recommends: coq (>= 8.0)
-Description: proof assistant for higher-order logic (Coq 7 theories)
- Coq is a proof assistant for higher-order logic, which allows the
- development of computer programs consistent with their formal
- specification. It is developed using Objective Caml and Camlp4.
- For more information, see <http://coq.inria.fr/>.
- .
- This package provides existing theories from Coq 7 in Coq 8, and
- allows proofs that were developed in Coq 7 to be used in Coq 8.
- It is also required to translate theories in Coq 7 syntax into
- the new syntax introduced in Coq 8. However, this package does
- not need to be installed to use Coq 7.
diff --git a/debian/copyright b/debian/copyright
index c53b8733..f0856000 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -14,9 +14,9 @@ INRIA-CNRS, University Paris Sud, All rights reserved.
 This product includes also software developed by
         Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
           parsing/search.ml)
-        Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
+        Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
         Pierre Courtieu, Lemme (contrib/funind)
-        Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
+        Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
         Claudio Sacerdoti Coen, HELM, University of Bologna (contrib/xml)
 
 Coq includes a tactic Jp based on JProver, a theorem prover for
@@ -27,13 +27,13 @@ and then integrated it into Coq.
         
 The Coq development Team (march 2004)
         Bruno Barras (INRIA)
-        Pierre Corbineau (Université Paris Sud)
-        Jean-Christophe Filliâtre (CNRS)
+        Pierre Corbineau (Université Paris Sud)
+        Jean-Christophe Filliâtre (CNRS)
         Hugo Herbelin (INRIA)
-        Pierre Letouzey (Université Paris Sud)
-        Claude Marché (Université Paris Sud-INRIA)
-        Christine Paulin (Université Paris Sud) 
-        Clément Renard (INRIA)
+        Pierre Letouzey (Université Paris Sud)
+        Claude Marché (Université Paris Sud-INRIA)
+        Christine Paulin (Université Paris Sud) 
+        Clément Renard (INRIA)
 
 The complete list of developpers and contributors can be found in
 /usr/share/doc/doc/CREDITS.gz
diff --git a/debian/coq-libs.install b/debian/coq-libs.install
index c721f0c8..653e2b54 100644
--- a/debian/coq-libs.install
+++ b/debian/coq-libs.install
@@ -1,4 +1,4 @@
 usr/lib/coq/contrib
 usr/lib/coq/states
 usr/lib/coq/theories
-usr/lib/coq/ide/utf8.vo usr/lib/coq
+usr/lib/coq/ide/utf8.vo	usr/lib/coq
diff --git a/debian/coq.install b/debian/coq.install
index d1182ab6..59bcb594 100644
--- a/debian/coq.install
+++ b/debian/coq.install
@@ -8,8 +8,11 @@ usr/bin/coq-tex
 usr/bin/coqtop*
 usr/bin/coqwc
 usr/bin/gallina
-usr/share/emacs/site-lisp/coq
-usr/share/emacs/site-lisp/coqdoc.sty
+usr/lib/coq/*.cma
+usr/lib/coq/*.cmxa
+usr/lib/coq/tools/coqdoc/
+usr/share/emacs/site-lisp/coq/*
 usr/share/man/man1/c*
 usr/share/man/man1/gallina.1
 usr/share/texmf/tex/latex/misc/*
+usr/share/emacs/site-lisp/coqdoc.sty    usr/share/texmf/tex/latex/misc/
diff --git a/debian/coq.xpm b/debian/coq.xpm
index e58ebad7..fe188d02 100644
--- a/debian/coq.xpm
+++ b/debian/coq.xpm
@@ -1,54 +1,52 @@
 /* XPM */
-static char *coq[] = {
-/* columns rows colors chars-per-pixel */
-"32 32 16 1",
-"  c #220C08",
-". c #342A2C",
-"X c #5A261F",
-"o c #6A4D4B",
-"O c #923827",
-"+ c #BF381C",
-"@ c #996252",
-"# c #837671",
-"$ c #D35E3A",
-"% c #CA7852",
-"& c #E19667",
-"* c #A59082",
-"= c #B9ADA8",
-"- c #EAB48F",
-"; c #F2D3B6",
-": c #FCFDF9",
-/* pixels */
-"::::::::::::::::::::::::::::::::",
-"::::::::::::::::::::::::::::::::",
-":::::X.:::::::::::::::::::::::::",
-"::::++-==:::::::::::::::::::::::",
-":::+;;+$:*::::::::::::::::::::::",
-":::;-++%:: :::::::::::::::::::::",
-":::*+++#:::;::::::::::::::::::::",
-"::::= +O::::::::::::::::::::::::",
-":::::: :::::o:::::::::::::::::::",
-"::::::=;:::::=::::::::::::::*:::",
-"::::::;::::::::: :::::::::::=:::",
-":::::=:::::::::::::::::: :::.:::",
-":::::*:::::::::::::.::.::::;X:::",
-":::::;::::::::::::::o:::;:-*.:::",
-"::::*;;;::::::;;:;-::--:;&&&X:::",
-"::::#;;;;-;;::;;;;;-;;--%%-%::::",
-":::::--;;@;;;;;-;-;--%oO%&% ::::",
-":::::.--;-@%&--&&%$$OOXO%%@:::::",
-"::::::o&--& O+XO&& XXX Oo ::::::",
-"::::::;@%%&%$  XX$X X Oo@ ::::::",
-"::::::::=O$OO+XX O X OO@ :::::::",
-"::::::::::;+X O%OOOOOOOo::::::::",
-"::::::::::::oOOXXX X  ::::::::::",
-":::::::::::::XX  X X::::::::::::",
-"::::::::::::::    .:::::::::::::",
-":::::::::::::: o:.::::::::::::::",
-":::::::::::::: #:.::::::::::::::",
-":::::::::::-oX%oo&*:::::::::::::",
-"::::::::::::o.#:::=@::::::::::::",
-"::::::::::::::::::::::::::::::::",
-"::::::::::::::::::::::::::::::::",
-"::::::::::::::::::::::::::::::::"
-};
+static char * coq_xpm[] = {
+"32 32 17 1",
+" 	c None",
+".	c #5A261F",
+"+	c #342A2C",
+"@	c #BF381C",
+"#	c #EAB48F",
+"$	c #B9ADA8",
+"%	c #F2D3B6",
+"&	c #D35E3A",
+"*	c #FCFDF9",
+"=	c #A59082",
+"-	c #CA7852",
+";	c #220C08",
+">	c #837671",
+",	c #923827",
+"'	c #6A4D4B",
+")	c #E19667",
+"!	c #996252",
+"                                ",
+"                                ",
+"     .+                         ",
+"    @@#$$                       ",
+"   @%%@&*=                      ",
+"   %#@@-**;                     ",
+"   =@@@>***                     ",
+"    $;@,****                    ",
+"      ;*****'                   ",
+"      $%*****$              =   ",
+"      %*********;         **$   ",
+"     $************      ;***+   ",
+"     =*************+**+****%.   ",
+"     %**************'***%*#=+   ",
+"    =%%%******%%*%#**##*%))).   ",
+"    >%%%%#%%**%%%%%#%%##--#-    ",
+"     ##%%!%%%%%#%#%##-',-)-;    ",
+"     +##%#!-)##))-&&,,.,--!     ",
+"      ')##);,@.,));...;,';      ",
+"       !--)-&;;..&.;.;,'!;      ",
+"        $,&,,@..;,;.;,,!;       ",
+"           @.;,-,,,,,,,'        ",
+"            ',,...;.;;          ",
+"             ..;;.;.            ",
+"              ;;;;+             ",
+"              ;' +              ",
+"              ;> +              ",
+"           #'.-'')=             ",
+"            '+>   $!            ",
+"                                ",
+"                                ",
+"                                "};
diff --git a/debian/coq7-libs.install b/debian/coq7-libs.install
deleted file mode 100644
index e888a17f..00000000
--- a/debian/coq7-libs.install
+++ /dev/null
@@ -1,3 +0,0 @@
-usr/lib/coq/contrib7
-usr/lib/coq/states7
-usr/lib/coq/theories7
diff --git a/debian/coqide.desktop b/debian/coqide.desktop
index 1515c273..c56bfec4 100644
--- a/debian/coqide.desktop
+++ b/debian/coqide.desktop
@@ -1,9 +1,9 @@
 [Desktop Entry]
 Encoding=UTF-8
-Name=CoqIde
+Name=CoqIDE Proof Assistant
 Comment=Graphical interface for the Coq proof assistant
-Exec=/usr/bin/coqide
+Exec=coqide
 Type=Application
-Categories=GTK;Science;Math;
+Categories=Application;Development;Science;Math;IDE;GTK;
 Terminal=false
-Icon=/usr/share/pixmaps/coq.xpm
+Icon=coq
diff --git a/debian/coqide.install b/debian/coqide.install
index 7df75581..f214e01c 100644
--- a/debian/coqide.install
+++ b/debian/coqide.install
@@ -1,5 +1,4 @@
 usr/bin/coqide*
-usr/lib/coq/ide/coq.ico
-usr/lib/coq/ide/coq2.ico
+usr/lib/coq/ide/coq.png
 usr/lib/coq/ide/utf8.vo
 usr/lib/coq/ide/.coqide-gtk2rc
diff --git a/debian/coqide.menu b/debian/coqide.menu
index 0fb1935a..2bf7d541 100644
--- a/debian/coqide.menu
+++ b/debian/coqide.menu
@@ -1,4 +1,4 @@
 ?package(coqide):command="/usr/bin/coqide" \
   icon="/usr/share/pixmaps/coqide.xpm" \
   needs="X11" \
-  section="Apps/Math" title="CoqIde"
+  section="Apps/Math" title="CoqIDE"
diff --git a/debian/patches/00list b/debian/patches/00list
index 3804c9ad..bbb91a76 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +1,6 @@
-coq-8.0pl3-ocaml-3.09
+coqdoc_stdlib
+browser
+makefile
+no-complexity-test
+configure
+cmxa-install
diff --git a/debian/patches/cmxa-install.dpatch b/debian/patches/cmxa-install.dpatch
new file mode 100755
index 00000000..7e8d2ffb
--- /dev/null
+++ b/debian/patches/cmxa-install.dpatch
@@ -0,0 +1,23 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## cmxa-install.dpatch by Samuel Mimram <smimram@debian.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: .cmxa are not generated on non-native archs, so don't install them.
+
+@DPATCH@
+diff -urNad coq-8.1+dfsg~/Makefile coq-8.1+dfsg/Makefile
+--- coq-8.1+dfsg~/Makefile	2007-02-18 13:25:29.000000000 +0100
++++ coq-8.1+dfsg/Makefile	2007-02-18 13:27:28.000000000 +0100
+@@ -1272,7 +1272,11 @@
+         parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \
+         parsing/highparsing.cma tactics/hightactics.cma contrib/contrib.cma
+ 
+-OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++ifeq ($(BEST),opt)
++  OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
++else
++  OBJECTCMXA=
++endif
+ 
+ install-library:
+ 	$(MKDIR) $(FULLCOQLIB)
diff --git a/debian/patches/configure.dpatch b/debian/patches/configure.dpatch
new file mode 100755
index 00000000..db3ef2a5
--- /dev/null
+++ b/debian/patches/configure.dpatch
@@ -0,0 +1,19 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## configure.dpatch by Pierre Letouzey <pierre.letouzey@pps.jussieu.fr>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Correctly detect whether ocamlopt is present or not.
+
+@DPATCH@
+diff -urNad coq-8.1+dfsg~/configure coq-8.1+dfsg/configure
+--- coq-8.1+dfsg~/configure	2007-02-10 08:32:28.000000000 +0000
++++ coq-8.1+dfsg/configure	2007-02-15 12:58:56.000000000 +0000
+@@ -340,7 +340,7 @@
+ # do we have a native compiler: test of ocamlopt and its version
+ 
+ if [ "$best_compiler" = "opt" ] ; then
+-  if test -e `which "$nativecamlc"` ; then
++  if test -e "`which $nativecamlc`" ; then
+       CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
+       if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
+ 	  echo "native and bytecode compilers do not have the same version!"; fi
diff --git a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
deleted file mode 100755
index 90b4d583..00000000
--- a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch
+++ /dev/null
@@ -1,507 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09.
-## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09
-
-@DPATCH@
-diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile
---- coq-8.0pl3~/Makefile	2006-01-11 23:18:05.000000000 +0000
-+++ coq-8.0pl3/Makefile	2006-02-19 11:28:43.000000000 +0000
-@@ -77,8 +77,8 @@
- 
- MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
- 
--BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG)
--OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF)
-+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y
-+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y
- OCAMLDEP=ocamldep
- DEPFLAGS=-slash $(LOCALINCLUDES)
- 
-diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml
---- coq-8.0pl3~/contrib/first-order/sequent.ml	2004-07-16 19:30:10.000000000 +0000
-+++ coq-8.0pl3/contrib/first-order/sequent.ml	2006-02-19 11:28:43.000000000 +0000
-@@ -6,7 +6,7 @@
- (*         *       GNU Lesser General Public License Version 2.1        *)
- (************************************************************************)
- 
--(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *)
-+(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *)
- 
- open Term
- open Util
-@@ -278,7 +278,7 @@
-   let h dbname=
-     let hdb=
-       try
--	Util.Stringmap.find dbname !searchtable 
-+	searchtable_map dbname 
-       with Not_found-> 
- 	error ("Firstorder: "^dbname^" : No such Hint database") in
-       Hint_db.iter g hdb in
-diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml
---- coq-8.0pl3~/contrib/interface/blast.ml	2004-07-16 19:30:11.000000000 +0000
-+++ coq-8.0pl3/contrib/interface/blast.ml	2006-02-19 11:28:43.000000000 +0000
-@@ -351,16 +351,16 @@
-   let db_list =
-     List.map
-       (fun x -> 
--	 try Stringmap.find x !searchtable
-+	 try searchtable_map x
- 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
-       ("core"::dbnames) 
-   in
-   tclTRY (e_search_auto debug np db_list)
- 
- let full_eauto debug n gl = 
--  let dbnames = stringmap_dom !searchtable in
-+  let dbnames = current_db_names () in
-   let dbnames =  list_subtract dbnames ["v62"] in
--  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-+  let db_list = List.map searchtable_map dbnames in
-   let local_db = make_local_hint_db gl in
-   tclTRY (e_search_auto debug n db_list) gl
- 
-@@ -369,8 +369,6 @@
- (**********************************************************************
-    copié de tactics/auto.ml on a juste modifié search_gen
- *)
--let searchtable_map name = 
--  Stringmap.find name !searchtable
- 
- (* local_db is a Hint database containing the hypotheses of current goal *)
- (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
-@@ -499,9 +497,9 @@
- let default_search_depth = ref 5
- 			     
- let full_auto n gl = 
--  let dbnames = stringmap_dom !searchtable in
-+  let dbnames = current_db_names () in
-   let dbnames = list_subtract dbnames ["v62"] in
--  let db_list = List.map (fun x -> searchtable_map x) dbnames in
-+  let db_list = List.map searchtable_map dbnames in
-   let hyps = pf_hyps gl in
-   tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
-   
-diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml
---- coq-8.0pl3~/interp/symbols.ml	2004-11-17 09:33:38.000000000 +0000
-+++ coq-8.0pl3/interp/symbols.ml	2006-02-19 11:28:43.000000000 +0000
-@@ -6,7 +6,7 @@
- (*         *       GNU Lesser General Public License Version 2.1        *)
- (************************************************************************)
- 
--(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *)
-+(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *)
- 
- (*i*)
- open Util
-@@ -43,18 +43,18 @@
- type delimiters = string
- 
- type scope = {
--  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
-+  notations: (string, interpretation * (dir_path * string) * bool) Gmap.t;
-   delimiters: delimiters option
- }
- 
- (* Uninterpreted notation map: notation -> level * dir_path *)
--let notation_level_map = ref Stringmap.empty
-+let notation_level_map = ref Gmap.empty
- 
- (* Scopes table: scope_name -> symbol_interpretation *)
--let scope_map = ref Stringmap.empty
-+let scope_map = ref Gmap.empty
- 
- let empty_scope = {
--  notations = Stringmap.empty;
-+  notations = Gmap.empty;
-   delimiters = None
- }
- 
-@@ -62,20 +62,20 @@
- let type_scope = "type_scope" (* special scope used for interpreting types *)
- 
- let init_scope_map () =
--  scope_map := Stringmap.add default_scope empty_scope !scope_map;
--  scope_map := Stringmap.add type_scope empty_scope !scope_map
-+  scope_map := Gmap.add default_scope empty_scope !scope_map;
-+  scope_map := Gmap.add type_scope empty_scope !scope_map
- 
- (**********************************************************************)
- (* Operations on scopes *)
- 
- let declare_scope scope =
--  try let _ = Stringmap.find scope !scope_map in ()
-+  try let _ = Gmap.find scope !scope_map in ()
-   with Not_found ->
- (*    Options.if_verbose message ("Creating scope "^scope);*)
--    scope_map := Stringmap.add scope empty_scope !scope_map
-+    scope_map := Gmap.add scope empty_scope !scope_map
- 
- let find_scope scope =
--  try Stringmap.find scope !scope_map
-+  try Gmap.find scope !scope_map
-   with Not_found -> error ("Scope "^scope^" is not declared")
- 
- let check_scope sc = let _ = find_scope sc in ()
-@@ -124,7 +124,7 @@
- (**********************************************************************)
- (* Delimiters *)
- 
--let delimiters_map = ref Stringmap.empty
-+let delimiters_map = ref Gmap.empty
- 
- let declare_delimiters scope key =
-   let sc = find_scope scope in
-@@ -134,15 +134,15 @@
-       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
-   end;
-   let sc = { sc with delimiters = Some key } in
--  scope_map := Stringmap.add scope sc !scope_map;
--  if Stringmap.mem key !delimiters_map then begin
--    let oldsc = Stringmap.find key !delimiters_map in
-+  scope_map := Gmap.add scope sc !scope_map;
-+  if Gmap.mem key !delimiters_map then begin
-+    let oldsc = Gmap.find key !delimiters_map in
-     Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
-   end;
--  delimiters_map := Stringmap.add key scope !delimiters_map
-+  delimiters_map := Gmap.add key scope !delimiters_map
- 
- let find_delimiters_scope loc key = 
--  try Stringmap.find key !delimiters_map
-+  try Gmap.find key !delimiters_map
-   with Not_found -> 
-     user_err_loc 
-     (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
-@@ -229,7 +229,7 @@
- let find_with_delimiters = function
-   | None -> None
-   | Some scope ->
--      match (Stringmap.find scope !scope_map).delimiters with
-+      match (Gmap.find scope !scope_map).delimiters with
- 	| Some key -> Some (Some scope, Some key)
- 	| None -> None
- 
-@@ -257,23 +257,23 @@
- (* Uninterpreted notation levels *)
- 
- let declare_notation_level ntn level =
--  if not !Options.v7 & Stringmap.mem ntn !notation_level_map then
-+  if not !Options.v7 & Gmap.mem ntn !notation_level_map then
-     error ("Notation "^ntn^" is already assigned a level");
--  notation_level_map := Stringmap.add ntn level !notation_level_map
-+  notation_level_map := Gmap.add ntn level !notation_level_map
- 
- let level_of_notation ntn =
--  Stringmap.find ntn !notation_level_map
-+  Gmap.find ntn !notation_level_map
- 
- (* The mapping between notations and their interpretation *)
- 
- let declare_notation_interpretation ntn scopt pat df pp8only =
-   let scope = match scopt with Some s -> s | None -> default_scope in
-   let sc = find_scope scope in
--  if Stringmap.mem ntn sc.notations && Options.is_verbose () then
-+  if Gmap.mem ntn sc.notations && Options.is_verbose () then
-     warning ("Notation "^ntn^" was already used"^
-     (if scopt = None then "" else " in scope "^scope));
--  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
--  scope_map := Stringmap.add scope sc !scope_map;
-+  let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in
-+  scope_map := Gmap.add scope sc !scope_map;
-   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
- 
- let declare_uninterpretation rule (metas,c as pat) =
-@@ -292,7 +292,7 @@
- let rec interp_notation loc ntn scopes =
-   let f sc =
-     let scope = find_scope sc in
--    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
-+    let (pat,df,pp8only) = Gmap.find ntn scope.notations in
-     if pp8only then raise Not_found;
-     pat,(df,if sc = default_scope then None else Some sc) in
-   try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
-@@ -308,7 +308,7 @@
- 
- let availability_of_notation (ntn_scope,ntn) scopes =
-   let f scope =
--    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
-+    Gmap.mem ntn (Gmap.find scope !scope_map).notations in
-   find_without_delimiters f (ntn_scope,Some ntn) scopes
- 
- let rec interp_numeral_gen loc f n = function
-@@ -356,8 +356,8 @@
- let exists_notation_in_scope scopt ntn r =
-   let scope = match scopt with Some s -> s | None -> default_scope in
-   try
--    let sc = Stringmap.find scope !scope_map in
--    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
-+    let sc = Gmap.find scope !scope_map in
-+    let (r',_,pp8only) = Gmap.find ntn sc.notations in
-     r' = r, pp8only
-   with Not_found -> false, false
- 
-@@ -487,14 +487,14 @@
- 
- let pr_named_scope prraw scope sc =
-  (if scope = default_scope then
--   match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with
-+   match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
-      | 0 -> str "No lonely notation"
-      | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
-   else 
-     str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
-   ++ fnl ()
-   ++ pr_scope_classes scope
--  ++ Stringmap.fold
-+  ++ Gmap.fold
-        (fun ntn ((_,r),(_,df),_) strm ->
- 	 pr_notation_info prraw df r ++ fnl () ++ strm)
-        sc.notations (mt ())
-@@ -502,12 +502,12 @@
- let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
- 
- let pr_scopes prraw =
-- Stringmap.fold 
-+ Gmap.fold 
-    (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
-    !scope_map (mt ())
- 
- let rec find_default ntn = function
--  | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations ->
-+  | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
-       Some scope
-   | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
-   | _::scopes -> find_default ntn scopes
-@@ -531,9 +531,9 @@
-     if String.contains ntn ' ' then (=) ntn
-     else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
-   let l =
--    Stringmap.fold 
-+    Gmap.fold 
-       (fun scope_name sc ->
--	Stringmap.fold (fun ntn ((_,r),df,_) l ->
-+	Gmap.fold (fun ntn ((_,r),df,_) l ->
- 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
-       map [] in
-   let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
-@@ -560,7 +560,7 @@
- 
- let collect_notation_in_scope scope sc known =
-   assert (scope <> default_scope);
--  Stringmap.fold
-+  Gmap.fold
-     (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
-       if List.mem ntn known then acc else ((df,r)::l,ntn::known))
-     sc.notations ([],known)
-@@ -578,7 +578,7 @@
- 	  if List.mem ntn knownntn then (all,knownntn)
- 	  else
- 	    let ((_,r),(_,df),_) =
--	      Stringmap.find ntn (find_scope default_scope).notations in
-+	      Gmap.find ntn (find_scope default_scope).notations in
- 	    let all' = match all with
- 	      | (s,lonelyntn)::rest when s = default_scope ->
- 		  (s,(df,r)::lonelyntn)::rest
-@@ -614,13 +614,13 @@
- 
- (* Concrete syntax for symbolic-extension table *)
- let printing_rules = 
--  ref (Stringmap.empty : unparsing_rule Stringmap.t)
-+  ref (Gmap.empty : (string, unparsing_rule) Gmap.t)
- 
- let declare_notation_printing_rule ntn unpl =
--  printing_rules := Stringmap.add ntn unpl !printing_rules
-+  printing_rules := Gmap.add ntn unpl !printing_rules
- 
- let find_notation_printing_rule ntn =
--  try Stringmap.find ntn !printing_rules
-+  try Gmap.find ntn !printing_rules
-   with Not_found -> anomaly ("No printing rule found for "^ntn)
- 
- (**********************************************************************)
-@@ -644,13 +644,13 @@
- let init () =
-   init_scope_map ();
- (*
--  scope_stack := Stringmap.empty
-+  scope_stack := Gmap.empty
-   arguments_scope := Refmap.empty
- *)
--  notation_level_map := Stringmap.empty;
--  delimiters_map := Stringmap.empty;
-+  notation_level_map := Gmap.empty;
-+  delimiters_map := Gmap.empty;
-   notations_key_table := Gmapl.empty;
--  printing_rules := Stringmap.empty;
-+  printing_rules := Gmap.empty;
-   class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
- 
- let _ = 
-diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml
---- coq-8.0pl3~/tactics/auto.ml	2005-05-15 12:47:04.000000000 +0000
-+++ coq-8.0pl3/tactics/auto.ml	2006-02-19 11:28:43.000000000 +0000
-@@ -6,7 +6,7 @@
- (*         *       GNU Lesser General Public License Version 2.1        *)
- (************************************************************************)
- 
--(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
-+(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *)
- 
- open Pp
- open Util
-@@ -134,24 +134,28 @@
- 
- end
- 
--type frozen_hint_db_table = Hint_db.t Stringmap.t 
-+module Hintdbmap = Gmap
- 
--type hint_db_table = Hint_db.t Stringmap.t ref
-+type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t 
-+
-+type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref
- 
- type hint_db_name = string
- 
--let searchtable = (ref Stringmap.empty : hint_db_table)
-+let searchtable = (ref Hintdbmap.empty : hint_db_table)
- 
- let searchtable_map name = 
--  Stringmap.find name !searchtable
-+  Hintdbmap.find name !searchtable
- let searchtable_add (name,db) = 
--  searchtable := Stringmap.add name db !searchtable
-+  searchtable := Hintdbmap.add name db !searchtable
-+let current_db_names () =
-+  Hintdbmap.dom !searchtable
- 
- (**************************************************************************)
- (*                       Definition of the summary                        *)
- (**************************************************************************)
- 
--let init     () = searchtable := Stringmap.empty
-+let init     () = searchtable := Hintdbmap.empty
- let freeze   () = !searchtable
- let unfreeze fs = searchtable := fs
- 
-@@ -498,7 +502,7 @@
- 
- (* Print all hints associated to head c in any database *)
- let fmt_hint_list_for_head c = 
--  let dbs = stringmap_to_list !searchtable in
-+  let dbs = Hintdbmap.to_list !searchtable in
-   let valid_dbs = 
-     map_succeed 
-       (fun (name,db) -> (name,db,Hint_db.map_all c db)) 
-@@ -523,7 +527,7 @@
-       | [] -> assert false 
-     in
-     let hd = head_of_constr_reference hdc in
--    let dbs = stringmap_to_list !searchtable in
-+    let dbs = Hintdbmap.to_list !searchtable in
-     let valid_dbs = 
-       if occur_existential cl then 
- 	map_succeed 
-@@ -568,7 +572,7 @@
-   
- (* displays all the hints of all databases *)
- let print_searchtable () =
--  Stringmap.iter
-+  Hintdbmap.iter
-     (fun name db ->
-        msg (str "In the database " ++ str name ++ fnl ());
-        print_hint_db db)
-@@ -693,7 +697,7 @@
-   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
-     
- let full_trivial gl =
--  let dbnames = stringmap_dom !searchtable in
-+  let dbnames = Hintdbmap.dom !searchtable in
-   let dbnames = list_subtract dbnames ["v62"] in
-   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
-@@ -798,7 +802,7 @@
- let default_auto = auto !default_search_depth []
- 
- let full_auto n gl = 
--  let dbnames = stringmap_dom !searchtable in
-+  let dbnames = Hintdbmap.dom !searchtable in
-   let dbnames = list_subtract dbnames ["v62"] in
-   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-   let hyps = pf_hyps gl in
-@@ -911,7 +915,7 @@
-       to_add empty_named_context in
-   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
-   let db = Hint_db.add_list db0 (make_local_hint_db g) in
--  super_search n [Stringmap.find "core" !searchtable] db argl g
-+  super_search n [Hintdbmap.find "core" !searchtable] db argl g
- 
- let superauto n to_add argl  = 
-   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
-diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli
---- coq-8.0pl3~/tactics/auto.mli	2005-01-21 16:41:52.000000000 +0000
-+++ coq-8.0pl3/tactics/auto.mli	2006-02-19 11:28:43.000000000 +0000
-@@ -6,7 +6,7 @@
- (*         *       GNU Lesser General Public License Version 2.1        *)
- (************************************************************************)
- 
--(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
-+(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*)
- 
- (*i*)
- open Util
-@@ -56,12 +56,16 @@
-     val iter : (constr_label -> stored_data list -> unit) -> t -> unit
-   end
- 
--type frozen_hint_db_table = Hint_db.t Stringmap.t
-+type frozen_hint_db_table
- 
--type hint_db_table = Hint_db.t Stringmap.t ref
-+type hint_db_table
- 
- type hint_db_name = string
- 
-+val searchtable_map : hint_db_name -> Hint_db.t
-+
-+val current_db_names : unit -> hint_db_name list
-+
- val add_hints : locality_flag -> hint_db_name list -> hints -> unit
- 
- val print_searchtable : unit -> unit
-diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4
---- coq-8.0pl3~/tactics/eauto.ml4	2004-07-16 19:30:52.000000000 +0000
-+++ coq-8.0pl3/tactics/eauto.ml4	2006-02-19 11:28:43.000000000 +0000
-@@ -8,7 +8,7 @@
- 
- (*i camlp4deps: "parsing/grammar.cma" i*)
- 
--(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
-+(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *)
- 
- open Pp
- open Util
-@@ -391,16 +391,16 @@
-   let db_list =
-     List.map
-       (fun x -> 
--	 try Stringmap.find x !searchtable
-+	 try searchtable_map x
- 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
-       ("core"::dbnames) 
-   in
-   tclTRY (e_search_auto debug np db_list)
- 
- let full_eauto debug n gl = 
--  let dbnames = stringmap_dom !searchtable in
-+  let dbnames = current_db_names () in
-   let dbnames =  list_subtract dbnames ["v62"] in
--  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-+  let db_list = List.map (fun x -> searchtable_map x) dbnames in
-   let local_db = make_local_hint_db gl in
-   tclTRY (e_search_auto debug n db_list) gl
- 
diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch
new file mode 100644
index 00000000..bf89f1f7
--- /dev/null
+++ b/debian/patches/no-complexity-test.dpatch
@@ -0,0 +1,21 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: Don't run complexity tests, they are far too fragile.
+
+@DPATCH@
+diff -urNad coq-8.1gamma~/test-suite/check coq-8.1gamma/test-suite/check
+--- coq-8.1gamma~/test-suite/check	2006-11-03 14:07:27.000000000 +0100
++++ coq-8.1gamma/test-suite/check	2006-11-23 15:19:49.000000000 +0100
+@@ -145,8 +145,8 @@
+ test_parser parser
+ echo "Interactive tests"
+ test_interactive interactive
+-echo "Complexity tests"
+-test_complexity complexity
++echo "Skipping complexity tests"
++#test_complexity complexity
+ echo "Module tests"
+ $coqtop -compile modules/Nat
+ $coqtop -compile modules/plik
diff --git a/debian/rules b/debian/rules
index b4498d12..d8920943 100755
--- a/debian/rules
+++ b/debian/rules
@@ -10,11 +10,10 @@ export DH_OPTIONS
 # We want to use dpatch
 include /usr/share/dpatch/dpatch.make
 
-COQPREF=$(CURDIR)/debian/tmp
-ADDPREF=COQINSTALLPREFIX=$(COQPREF)
+COQPREF := $(CURDIR)/debian/tmp
+ADDPREF := COQINSTALLPREFIX=$(COQPREF)
 
-CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man \
-	--emacslib /usr/share/emacs/site-lisp/coq --reals all
+CONFIGUREOPTS := --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all
 
 configure: configure-stamp
 configure-stamp:
@@ -43,6 +42,13 @@ build-stamp:
 	else \
 		$(MAKE) BEST=byte HASCOQIDE=byte check; \
 	fi
+	if [ -e opt-stamp ]; then \
+		$(MAKE) BEST=opt glob.dump; \
+	else \
+		$(MAKE) BEST=byte HASCOQIDE=byte glob.dump; \
+	fi
+	cp tools/coqdoc/coqdoc.sty doc/stdlib/
+	$(MAKE) -C doc stdlib/html/index.html
 	touch build-stamp
 
 clean: unpatch
@@ -52,9 +58,11 @@ clean: unpatch
 
 	-$(MAKE) clean
 	-$(MAKE) archclean
-	rm -f bin/parser.opt
+	rm -f bin/*
 	rm -f tools/coqdoc/*.cm[oi]
 	rm -f config/coq_config.ml config/Makefile test-suite/check.log
+	rm -f dev/ocamldebug-v7
+	rm -f ide/undo.mli glob.dump
 
 	dh_clean
 
@@ -74,11 +82,10 @@ install: build
 		echo "Stripping: $$i"; \
 		strip -R .note -R .comment $$i; \
 	done
-	-for i in $(COQPREF)/usr/bin/coqide.*; do \
-		echo "Rpath for `chrpath $$i`"; \
-		echo "Removing rpath: $$i"; \
-		chrpath -d $$i; \
-	done
+	if [ -e opt-stamp ]; then \
+		strip -R .note -R .comment $ $(COQPREF)/usr/bin/coqc; \
+		strip -R .note -R .comment $(COQPREF)/usr/bin/coqmktop; \
+	fi
 	cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm
 	cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm
 	cp debian/coqide.desktop debian/coqide/usr/share/applications
@@ -96,7 +103,8 @@ install: build
 	cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1
 	cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1
 
-	chmod -x debian/tmp/usr/lib/coq/ide/coq2.ico
+	cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/
+	cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib
 
 	# These are installed as docs
 	rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ
@@ -111,6 +119,7 @@ binary-common:
 	dh_installemacsen
 	dh_installman
 	dh_installchangelogs CHANGES
+	dh_installtex
 	dh_desktop
 	dh_link
 	dh_compress
diff --git a/debian/utils/purify_tarball b/debian/utils/purify_tarball
new file mode 100755
index 00000000..ea7e08f1
--- /dev/null
+++ b/debian/utils/purify_tarball
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+set -e
+
+CURDIR=`pwd`
+ORIG=$1
+WORKDIR=`dirname $ORIG`
+ORIGFILE=`basename $ORIG`
+VERSION=`echo "$ORIGFILE" | sed "s/^coq-\([0-9\.]\+\)\.tar\.gz$/\1/"`
+
+cd $WORKDIR
+
+tar zxf $ORIGFILE
+
+rm -rf coq-$VERSION/doc/common
+rm -rf coq-$VERSION/doc/faq
+rm -rf coq-$VERSION/doc/RecTutorial
+rm -rf coq-$VERSION/doc/refman
+rm -rf coq-$VERSION/doc/rt
+rm -rf coq-$VERSION/doc/tools
+rm -rf coq-$VERSION/doc/tutorial
+
+tar zcf coq_$VERSION+dfsg.orig.tar.gz coq-$VERSION/
+rm -rf coq-$VERSION
+
+cd $CURDIR
diff --git a/debian/watch b/debian/watch
index 8867705d..45c97702 100644
--- a/debian/watch
+++ b/debian/watch
@@ -1,2 +1,2 @@
-version=2
+version=3
 ftp://ftp.inria.fr/INRIA/coq/current/coq-([0-9a-z\.]*)\.tar\.gz debian uupdate