Move interning the [hint_pattern] outside the Typeclasses hooks.

Close #7562.

[api] move hint_info ast to tactics.

2 files changed, 11 insertions, 11 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 12a944d32..70588b6ad 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
 
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
@@ -80,7 +80,7 @@ type typeclass = {
   cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
-  cl_projs : (Name.t * (direction * hint_info_expr) option
+  cl_projs : (Name.t * (direction * hint_info) option
 	      * Constant.t option) list;
   
   cl_strict : bool;
@@ -92,7 +92,7 @@ type typeclasses = typeclass Refmap.t
 
 type instance = {
   is_class: GlobRef.t;
-  is_info: hint_info_expr;
+  is_info: hint_info;
   (* Sections where the instance should be redeclared,
      None for discard, Some 0 for none. *)
   is_global: int option;
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 2a8e0b874..c78382c82 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
 
 (** This module defines type-classes *)
 type typeclass = {
@@ -44,7 +44,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (Name.t * (direction * hint_info_expr) option * Constant.t option) list;
+  cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list;
 
   (** Whether we use matching or full unification during resolution *)
   cl_strict : bool; 
@@ -62,7 +62,7 @@ val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
-val new_instance : typeclass -> hint_info_expr -> bool -> GlobRef.t -> instance
+val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
 val add_instance : instance -> unit
 val remove_instance : instance -> unit
 
@@ -129,16 +129,16 @@ val classes_transparent_state : unit -> transparent_state
 
 val add_instance_hint_hook :
   (global_reference_or_constr -> GlobRef.t list ->
-   bool (* local? *) -> hint_info_expr -> Decl_kinds.polymorphic -> unit) Hook.t
+   bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
 val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
-  bool -> hint_info_expr -> Decl_kinds.polymorphic -> unit
+  bool -> hint_info -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : GlobRef.t -> unit
 
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
+val declare_instance : hint_info option -> bool -> GlobRef.t -> unit
 
 
 (** Build the subinstances hints for a given typeclass object.
@@ -146,5 +146,5 @@ val declare_instance : hint_info_expr option -> bool -> GlobRef.t -> unit
     subinstances and add only the missing ones. *)
 
 val build_subclasses : check:bool -> env -> evar_map -> GlobRef.t ->
-                       hint_info_expr ->
-                       (GlobRef.t list * hint_info_expr * constr) list
+                       hint_info ->
+                       (GlobRef.t list * hint_info * constr) list