Move interning the [hint_pattern] outside the Typeclasses hooks.

Close #7562.

[api] move hint_info ast to tactics.

3 files changed, 11 insertions, 13 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3e08c6d87..1ddb1a2bf 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -546,12 +546,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
           let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in
             (List.map_append
              (fun (path,info,c) ->
-	      let info =
-                { info with hint_pattern =
-                            Option.map (Constrintern.intern_constr_pattern env sigma)
-                                       info.hint_pattern }
-	      in
-	      make_resolves env sigma ~name:(PathHints path)
+              make_resolves env sigma ~name:(PathHints path)
                   (true,false,not !Flags.quiet) info false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b5be4c1c..40cbfa5ab 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Libobject
 open Namegen
 open Libnames
 open Smartlocate
-open Misctypes
 open Termops
 open Inductiveops
 open Typing
@@ -100,6 +99,8 @@ let empty_hint_info =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -165,7 +166,7 @@ type hint_mode =
   | ModeOutput (* Anything *)
 
 type hints_expr =
-  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
@@ -1235,7 +1236,7 @@ let add_trivials env sigma l local dbnames =
 
 type hnf = bool
 
-type hint_info = (patvar list * constr_pattern) hint_info_gen
+type nonrec hint_info = hint_info
 
 type hints_entry =
   | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f05988703..7ef7f0185 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -14,10 +14,10 @@ open EConstr
 open Environ
 open Decl_kinds
 open Evd
-open Misctypes
 open Tactypes
 open Clenv
 open Pattern
+open Typeclasses
 
 (** {6 General functions. } *)
 
@@ -33,6 +33,8 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen
 
 (** Pre-created hint databases *)
 
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -80,7 +82,7 @@ type hint_mode =
   | ModeOutput (* Anything *)
 
 type hints_expr =
-  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
   | HintsImmediate of reference_or_constr list
   | HintsUnfold of Libnames.reference list
   | HintsTransparency of Libnames.reference list * bool
@@ -160,8 +162,6 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
-type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen
-
 type hint_term =
   | IsGlobRef of GlobRef.t
   | IsConstr of constr * Univ.ContextSet.t
@@ -290,3 +290,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t
 (** Hook for changing the initialization of auto *)
 val add_hints_init : (unit -> unit) -> unit
 
+type nonrec hint_info = hint_info
+[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]