Move interning the [hint_pattern] outside the Typeclasses hooks.

Close #7562.

[api] move hint_info ast to tactics.

4 files changed, 19 insertions, 15 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 40001c0a37..c822089806 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -50,11 +50,6 @@ let _ =
      let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
-     let info =
-       { info with hint_pattern =
-		   Option.map
-                     (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env())))
-		     info.hint_pattern } in
      Flags.silently (fun () ->
        Hints.add_hints ~local [typeclasses_db]
 	  (Hints.HintsResolveEntry
@@ -63,10 +58,17 @@ let _ =
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
 
+let intern_info {hint_priority;hint_pattern} =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in
+  {hint_priority;hint_pattern}
+
 (** TODO: add subinstances *)
 let existing_instance glob g info =
   let c = global g in
   let info = Option.default Hints.empty_hint_info info in
+  let info = intern_info info in
   let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
   let _, r = Term.decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
@@ -107,6 +109,7 @@ open Pp
 
 let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
+  let info = intern_info info in
   Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
@@ -301,7 +304,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
             if program_mode then
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+                  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+                  let pri = intern_info pri in
 		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
 	      in
 	      let obls, constr, typ =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 27d3a4669d..631da8400a 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,12 +22,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> hint_info_expr option -> unit
+val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  hint_info_expr -> (** priority *)
+  Hints.hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(GlobRef.t -> unit) ->
@@ -51,7 +51,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(GlobRef.t -> unit) ->
-  hint_info_expr ->
+  Hints.hint_info_expr ->
   Id.t
 
 (** Setting opacity *)
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 9d999793e8..2993a1661b 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -25,7 +25,7 @@ module Vernac_ :
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
-    val hint_info : Typeclasses.hint_info_expr Gram.entry
+    val hint_info : Hints.hint_info_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index cf0da4de22..40fab1f9cd 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -119,11 +119,11 @@ type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
       hint_pattern : 'a option }
 [@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"]
 
-type hint_info_expr = Typeclasses.hint_info_expr
-[@@ocaml.deprecated "Please use [Typeclasses.hint_info_expr]"]
+type hint_info_expr = Hints.hint_info_expr
+[@@ocaml.deprecated "Please use [Hints.hint_info_expr]"]
 
 type hints_expr = Hints.hints_expr =
-  | HintsResolve of (Typeclasses.hint_info_expr * bool * Hints.reference_or_constr) list
+  | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
   | HintsImmediate of Hints.reference_or_constr list
   | HintsUnfold of reference list
   | HintsTransparency of reference list * bool
@@ -362,12 +362,12 @@ type nonrec vernac_expr =
       local_binder_expr list * (* super *)
         typeclass_constraint * (* instance name, class name, params *)
         (bool * constr_expr) option * (* props *)
-        Typeclasses.hint_info_expr
+        Hints.hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
-    (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *)
+    (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacDeclareClass of reference (* inductive or definition name *)