Suppression de la dépendance en Map.fold de ocaml dont la sémantique a

changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre
d'application des Hints de auto)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 26 insertions, 22 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index cc6dc33e62..9d3a5a2881 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -136,24 +136,28 @@ module Hint_db = struct
 
 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 @@ let fmt_hints_db (name,db,hintlist) =
 
 (* 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 @@ let fmt_hint_term cl =
       | [] -> 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 @@ let print_hint_db_by_name dbname =
   
 (* 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)
@@ -689,7 +693,7 @@ let trivial dbnames gl =
   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
@@ -791,7 +795,7 @@ let auto n dbnames gl =
 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
@@ -904,7 +908,7 @@ let search_superauto n to_add argl g =
       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 --git a/tactics/auto.mli b/tactics/auto.mli
index 7442c34d32..6333e088b8 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -57,11 +57,11 @@ module Hint_db :
     val iter : (global_reference -> stored_data list -> unit) -> t -> unit
   end
 
-type frozen_hint_db_table = Hint_db.t Stringmap.t
+type hint_db_name = string
 
-type hint_db_table = Hint_db.t Stringmap.t ref
+val searchtable_map : hint_db_name -> Hint_db.t
 
-type hint_db_name = string
+val current_db_names : unit -> hint_db_name list
 
 val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
@@ -73,8 +73,6 @@ val print_hint_ref : global_reference -> unit
 
 val print_hint_db_by_name : hint_db_name -> unit
 
-val searchtable : hint_db_table
-
 (* [make_exact_entry hint_name (c, ctyp)]. 
    [hint_name] is the name of then hint;
    [c] is the term given as an exact proof to solve the goal;
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0a611e6552..d92c4f2ed2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -365,16 +365,16 @@ let eauto debug np dbnames =
   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
 
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index dbda5fd25d..57f6a4171f 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -10,9 +10,10 @@
 open Term
 open Proof_type
 open Tacexpr
+open Auto
 (*i*)
 
-val rawwit_hintbases : string list option raw_abstract_argument_type
+val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
 val e_assumption : tactic
 
@@ -24,4 +25,5 @@ val vernac_e_resolve_constr :  constr -> tactic
 
 val e_give_exact_constr : constr -> tactic
 
-val gen_eauto : bool -> bool * int -> Util.Stringmap.key list option -> tactic
+val gen_eauto : bool -> bool * int -> hint_db_name list option -> tactic
+