Finish patch for Hint Resolve, stopping to generate new constant names for

hints. 


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

1 files changed, 3 insertions, 3 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 43caf3fa3..618ec2bc0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -24,6 +24,7 @@ open Constrexpr
 
 open Decl_kinds
 open Entries
+open Misctypes
 
 let typeclasses_db = "typeclass_instances"
 
@@ -33,12 +34,11 @@ let set_typeclass_transparency c local b =
     
 let _ =
   Typeclasses.register_add_instance_hint
-    (fun inst local pri ->
-     let path = try Auto.PathHints [inst] with _ -> Auto.PathAny in
+    (fun inst path local pri ->
       Flags.silently (fun () ->
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
-	     [pri, false, path, inst])) ());
+	     [pri, false, Auto.PathHints path, inst])) ());
   Typeclasses.register_set_typeclass_transparency set_typeclass_transparency;
   Typeclasses.register_classes_transparent_state 
     (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))