Reverted 13293 commited mistakenly. Sorry for the noise.

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

1 files changed, 1 insertions, 25 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ba38f54584..0448b0b224 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -402,35 +402,12 @@ type hint_action = | CreateDB of bool * transparent_state
 		   | AddTransparency of evaluable_global_reference list * bool
 		   | AddTactic of (global_reference option * pri_auto_tactic) list
 
-let automatically_import_hints = ref false
-
-open Goptions
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optname  = "automatic importation of hints";
-      optkey   = ["Automatic";"Hints";"Importation"];
-      optread  = (fun () -> !automatically_import_hints);
-      optwrite = (:=) automatically_import_hints }
-
 let cache_autohint (_,(local,name,hints)) =
   match hints with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddTactic hints -> add_hint name hints
 
-let load_autohint _ x =
-  if
-    !automatically_import_hints || Flags.version_less_or_equal Flags.V8_2
-  then
-    cache_autohint x
-
-let open_autohint _ x =
-  if
-    not (!automatically_import_hints || Flags.version_less_or_equal Flags.V8_2)
-  then
-    cache_autohint x
-
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
 
@@ -523,8 +500,7 @@ let discharge_autohint (_,(local,name,hintlist as obj)) =
 let (inAutoHint,_) =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
-		    open_function = open_autohint;
-		    load_function = load_autohint;
+		    load_function = (fun _ -> cache_autohint);
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint }