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

1 files changed, 3 insertions, 5 deletions

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;