Started to package the upcoming 8.1 release.

12 files changed, 110 insertions, 538 deletions

diff --git a/debian/changelog b/debian/changelog
index afb42a67..b60769ed 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,13 @@
+coq (8.0pl3+8.1alpha-1) experimental; urgency=low
+
+  * New upstream release.
+  * Disabling checks for now as they don't succeed.
+  * Removed coq-8.0pl3-ocaml-3.09.dpatch.
+  * No longer providing the compatibility coq7-libs package.
+  * coq-libs is now providing its documentation in html format.
+
+ -- 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 9ec22d2f..bd35a5ba 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.6.2
-Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath
+Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath, tetex-bin
 
 Package: coq
 Architecture: any
@@ -39,7 +39,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
@@ -48,18 +48,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/coq-libs.dirs b/debian/coq-libs.dirs
new file mode 100644
index 00000000..aadcf27a
--- /dev/null
+++ b/debian/coq-libs.dirs
@@ -0,0 +1,2 @@
+usr/share/doc/coq-libs
+usr/share/doc/coq
diff --git a/debian/coq-libs.doc-base b/debian/coq-libs.doc-base
new file mode 100644
index 00000000..1a62a262
--- /dev/null
+++ b/debian/coq-libs.doc-base
@@ -0,0 +1,9 @@
+Document: coq-library
+Title: The Coq Standard Library
+Author: The Coq Development Team
+Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification.
+Section: Apps/Math
+
+Format: HTML
+Index: /usr/share/doc/coq-libs/html/index.html
+Files: /usr/share/doc/coq-libs/html/*.html
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..155e13af 100644
--- a/debian/coq.install
+++ b/debian/coq.install
@@ -9,7 +9,6 @@ usr/bin/coqtop*
 usr/bin/coqwc
 usr/bin/gallina
 usr/share/emacs/site-lisp/coq
-usr/share/emacs/site-lisp/coqdoc.sty
 usr/share/man/man1/c*
 usr/share/man/man1/gallina.1
 usr/share/texmf/tex/latex/misc/*
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.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/patches/00list b/debian/patches/00list
index 3804c9ad..fa82f62e 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1 +1 @@
-coq-8.0pl3-ocaml-3.09
+coqdoc_stdlib
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/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch
new file mode 100755
index 00000000..d81ce3c8
--- /dev/null
+++ b/debian/patches/coqdoc_stdlib.dpatch
@@ -0,0 +1,72 @@
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## coqdoc_stdlib.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.0pl3+8.1alpha~/doc/Makefile coq-8.0pl3+8.1alpha/doc/Makefile
+--- coq-8.0pl3+8.1alpha~/doc/Makefile	2006-04-07 15:08:12.000000000 +0000
++++ coq-8.0pl3+8.1alpha/doc/Makefile	2006-04-28 13:43:28.000000000 +0000
+@@ -216,6 +216,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)
+ 	mv stdlib/html/index.html stdlib/index-body.html
+ 
+@@ -232,6 +233,7 @@
+ stdlib/Library.coqdoc.tex: 
+ 	(for dir in $(LIBDIRS) ; do \
+ 	  $(COQDOC) -q --gallina --body-only --latex --stdout \
++	    --coqlib_path $(COQTOP) \
+             -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done)
+ 
+ stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex
+diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml
+--- coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml	2006-03-08 10:47:12.000000000 +0000
++++ coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml	2006-04-28 13:41:09.000000000 +0000
+@@ -44,6 +44,7 @@
+ let title = ref ""
+ let externals = ref true
+ let coqlib = ref "http://coq.inria.fr/library/"
++let coqlib_path = ref Coq_config.coqlib
+ let raw_comments = ref false
+ 
+ let charset = ref "iso-8859-1"
+diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml
+--- coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml	2006-03-28 17:34:15.000000000 +0000
++++ coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml	2006-04-28 13:41:09.000000000 +0000
+@@ -54,6 +54,8 @@
+   prerr_endline "  --no-externals      no links to Coq standard library";
+   prerr_endline "  --coqlib <url>      set URL for Coq standard library";
+   prerr_endline "                      (default is http://coq.inria.fr/library/)";
++  prerr_endline "  --coqlib_path <dir> path of the coqlibrary";
++  prerr_endline ("                      (default is " ^ !Cdglobals.coqlib_path ^ ")");
+   prerr_endline "  -R <dir> <coqdir>   map physical dir to Coq dir";
+   prerr_endline "  --latin1            set ISO-8859-1 input language";
+   prerr_endline "  --utf8              set UTF-8 input language";
+@@ -315,6 +317,8 @@
+ 	Cdglobals.externals := false; parse_rec rem
+     | ("--coqlib" | "-coqlib") :: u :: rem ->
+ 	Cdglobals.coqlib := u; parse_rec rem
++    | ("--coqlib_path" | "-coqlib_path") :: u :: rem ->
++        Cdglobals.coqlib_path := u; parse_rec rem
+     | ("--coqlib" | "-coqlib") :: [] ->
+ 	usage ()
+     | f :: rem -> 
+@@ -420,11 +424,11 @@
+ let produce_document l =
+   List.iter index_module l;
+   (if !target_language=HTML then
+-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in
++    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
+     let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
+       copy src dst);
+   (if !target_language=LaTeX then
+-    let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in
++    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
+     let dst = if !output_dir <> "" then 
+       Filename.concat !output_dir "coqdoc.sty" 
+     else "coqdoc.sty" in
diff --git a/debian/rules b/debian/rules
index b4498d12..2971382b 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
 
 configure: configure-stamp
 configure-stamp:
@@ -30,7 +29,8 @@ configure-stamp:
 build: patch-stamp configure-stamp build-stamp
 build-stamp:
 	dh_testdir
-	if grep -q BEST=opt config/Makefile; \
+	$(MAKE) world
+#	if grep -q BEST=opt config/Makefile; \
 	then \
 		($(MAKE) check \
 		   && touch opt-stamp) \
@@ -43,6 +43,9 @@ build-stamp:
 	else \
 		$(MAKE) BEST=byte HASCOQIDE=byte check; \
 	fi
+	$(MAKE) glob.dump
+	cp tools/coqdoc/coqdoc.sty doc/stdlib/
+	$(MAKE) -C doc stdlib
 	touch build-stamp
 
 clean: unpatch
@@ -55,6 +58,8 @@ clean: unpatch
 	rm -f bin/parser.opt
 	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
 
@@ -96,7 +101,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