Splitting out of auto.ml a file hints.ml dedicated to hints so as to

being able to export hints without tactics, vm, etc. to come with.

Some functions moved to the new proof engine.

3 files changed, 19 insertions, 19 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8f36fc79fe..4d23a41818 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -28,22 +28,22 @@ open Entries
 let typeclasses_db = "typeclass_instances"
 
 let set_typeclass_transparency c local b = 
-  Auto.add_hints local [typeclasses_db] 
-    (Auto.HintsTransparencyEntry ([c], b))
+  Hints.add_hints local [typeclasses_db] 
+    (Hints.HintsTransparencyEntry ([c], b))
     
 let _ =
   Hook.set Typeclasses.add_instance_hint_hook
     (fun inst path local pri poly ->
-     let inst' = match inst with IsConstr c -> Auto.IsConstr (c, Univ.ContextSet.empty)
-       | IsGlobal gr -> Auto.IsGlobRef gr
+     let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
+       | IsGlobal gr -> Hints.IsGlobRef gr
      in
       Flags.silently (fun () ->
-	Auto.add_hints local [typeclasses_db]
-	  (Auto.HintsResolveEntry
-	     [pri, poly, false, Auto.PathHints path, inst'])) ());
+	Hints.add_hints local [typeclasses_db]
+	  (Hints.HintsResolveEntry
+	     [pri, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook
-    (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
+    (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
         
 (** TODO: add subinstances *)
 let existing_instance glob g pri =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 2ac4339c16..b303533e48 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -632,8 +632,8 @@ let declare_obligation prg obl body ty uctx =
 	(DefinitionEntry ce,IsProof Property)
       in
 	if not opaque then
-	  Auto.add_hints false [Id.to_string prg.prg_name]
-	    (Auto.HintsUnfoldEntry [EvalConstRef constant]);
+	  Hints.add_hints false [Id.to_string prg.prg_name]
+	    (Hints.HintsUnfoldEntry [EvalConstRef constant]);
 	definition_message obl.obl_name;
 	{ obl with obl_body = 
 	    if poly then 
@@ -813,8 +813,8 @@ let rec solve_obligation prg num tac =
 			else DefinedObl cst
 		  in
 		    if transparent then
-		      Auto.add_hints true [Id.to_string prg.prg_name]
-			(Auto.HintsUnfoldEntry [EvalConstRef cst]);
+		      Hints.add_hints true [Id.to_string prg.prg_name]
+			(Hints.HintsUnfoldEntry [EvalConstRef cst]);
 		    { obl with obl_body = Some body }
 		in
 		let obls = Array.copy obls in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 63253d54ea..f6bc8bbebe 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -967,15 +967,15 @@ let vernac_declare_tactic_definition locality (x,def) =
 
 let vernac_create_hintdb locality id b =
   let local = make_module_locality locality in
-  Auto.create_hint_db local id full_transparent_state b
+  Hints.create_hint_db local id full_transparent_state b
 
 let vernac_remove_hints locality dbs ids =
   let local = make_module_locality locality in
-  Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
+  Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
 
 let vernac_hints locality poly local lb h =
   let local = enforce_module_locality locality local in
-  Auto.add_hints local lb (Auto.interp_hints poly h)
+  Hints.add_hints local lb (Hints.interp_hints poly h)
 
 let vernac_syntactic_definition locality lid x local y =
   Dumpglob.dump_definition lid false "syndef";
@@ -1528,11 +1528,11 @@ let vernac_print = function
     let univ = if b then Univ.sort_universes univ else univ in
     msg_notice (Univ.pr_universes univ)
   | PrintUniverses (b, Some s) -> dump_universes b s
-  | PrintHint r -> msg_notice (Auto.pr_hint_ref (smart_global r))
-  | PrintHintGoal -> msg_notice (Auto.pr_applicable_hint ())
-  | PrintHintDbName s -> msg_notice (Auto.pr_hint_db_by_name s)
+  | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+  | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
+  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
   | PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s)
-  | PrintHintDb -> msg_notice (Auto.pr_searchtable ())
+  | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
   | PrintScopes ->
       msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
   | PrintScope s ->