#! /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