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, 5 insertions, 6 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 729cbb2ad..72b3bbd27 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -103,13 +103,12 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val register_classes_transparent_state : (unit -> transparent_state) -> unit
 val classes_transparent_state : unit -> transparent_state
 
-val register_declare_definition : (?internal:bool -> ?opaque:bool -> ?kind:definition_object_kind -> identifier -> ?types:constr -> constr -> constant) -> unit
-
-
 val register_add_instance_hint : 
-  (global_reference -> bool (* local? *) -> int option -> unit) -> unit
+  (global_reference_or_constr -> global_reference list -> 
+   bool (* local? *) -> int option -> unit) -> unit
 val register_remove_instance_hint : (global_reference -> unit) -> unit
-val add_instance_hint : global_reference -> bool -> int option -> unit
+val add_instance_hint : global_reference_or_constr -> global_reference list -> 
+  bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
 
 val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
@@ -123,4 +122,4 @@ val declare_instance : int option -> bool -> global_reference -> unit
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) ->
-  (int option * global_reference) list
+  (global_reference list * int option * constr) list