[hints] Move and split Hint Declaration AST to vernac

This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.

13 files changed, 220 insertions, 156 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index e713ab13b2..5baa23b3e9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-        { Hints.HintsExtern (n,c, in_tac tac) } ] ]
+        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffb0e030db..0499ba200e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Globnames
 open Libobject
 open Namegen
 open Libnames
-open Smartlocate
 open Termops
 open Inductiveops
 open Typeclasses
@@ -100,8 +99,6 @@ 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 *)
@@ -164,10 +161,6 @@ type full_hint = hint with_metadata
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
-type reference_or_constr =
-  | HintsReference of qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -178,16 +171,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of qualid list
-  | HintsTransparency of qualid hints_transparency_target * bool
-  | HintsMode of qualid * hint_mode list
-  | HintsConstructors of qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type import_level = HintLax | HintWarn | HintStrict
 
 let warn_hint_to_string = function
@@ -1310,114 +1293,6 @@ let prepare_hint check env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     (c', diff)
 
-let project_hint ~poly pri l2r r =
-  let open EConstr in
-  let open Coqlib in
-  let gr = Smartlocate.global_with_alias r in
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma c in
-  let t =
-    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in
-  let sign,ccl = decompose_prod_assum sigma t in
-  let (a,b) = match snd (decompose_app sigma ccl) with
-    | [a;b] -> (a,b)
-    | _ -> assert false in
-  let p =
-    if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
-  let sigma, p = Evd.fresh_global env sigma p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
-  let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in
-  let name =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let ctx = Evd.univ_entry ~poly sigma in
-  let c = EConstr.to_constr sigma c in
-  let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in
-  let c = Declare.declare_constant
-      ~local:Declare.ImportDefaultBehavior
-      ~name ~kind:Decls.(IsDefinition Definition) cb
-  in
-  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
-
-let warn_deprecated_hint_constr =
-  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
-         (fun () ->
-           Pp.strbrk
-             "Declaring arbitrary terms as hints is deprecated; declare a global reference instead"
-         )
-
-let interp_hints ~poly =
-  fun h ->
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let f poly c =
-    let evd,c = Constrintern.interp_open_constr env sigma c in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let (c, diff) = prepare_hint true env sigma (evd,c) in
-    if poly then IsConstr (c, diff)
-    else
-      let () = Declare.declare_universe_context ~poly:false diff in
-      IsConstr (c, Univ.ContextSet.empty)
-  in
-  let fref r =
-    let gr = global_with_alias r in
-    Dumpglob.add_glob ?loc:r.CAst.loc gr;
-    gr in
-  let fr r = evaluable_of_global_reference env (fref r) in
-  let fi c =
-    match c with
-    | HintsReference c ->
-      let gr = global_with_alias c in
-        (PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c ->
-      let () = warn_deprecated_hint_constr () in
-      (PathAny, poly, f poly c)
-  in
-  let fp = Constrintern.intern_constr_pattern env sigma in
-  let fres (info, b, r) =
-    let path, poly, gr = fi r in
-    let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
-      (info, poly, b, path, gr)
-  in
-  let ft = function
-    | HintsVariables -> HintsVariables
-    | HintsConstants -> HintsConstants
-    | HintsReferences lhints -> HintsReferences (List.map fr lhints)
-  in
-  let fp = Constrintern.intern_constr_pattern (Global.env()) in
-  match h with
-  | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
-  | HintsResolveIFF (l2r, lc, n) ->
-    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
-  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
-  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
-  | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
-  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
-  | HintsConstructors lqid ->
-      let constr_hints_of_ind qid =
-        let ind = global_inductive_with_alias qid in
-        let mib,_ = Global.lookup_inductive ind in
-        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
-          List.init (nconstructors env ind)
-            (fun i -> let c = (ind,i+1) in
-                      let gr = GlobRef.ConstructRef c in
-                        empty_hint_info,
-                        (Declareops.inductive_is_polymorphic mib), true,
-                        PathHints [gr], IsGlobRef gr)
-      in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
-  | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (fp sigma) patcom in
-      let l = match pat with None -> [] | Some (l, _) -> l in
-      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
-      let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
-      let _, tacexp = Genintern.generic_intern env tacexp in
-      HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-
 let add_hints ~locality dbnames h =
   let local, superglobal = match locality with
   | Goptions.OptDefault | Goptions.OptGlobal -> false, true
diff --git a/tactics/hints.mli b/tactics/hints.mli
index eed0e37fac..a54da8ef0a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -32,8 +32,6 @@ 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 *)
@@ -78,10 +76,6 @@ type search_entry
 
 type hint_entry
 
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -92,16 +86,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.qualid list
-  | HintsTransparency of Libnames.qualid hints_transparency_target * bool
-  | HintsMode of Libnames.qualid * hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
   | PathStar of 'a hints_path_gen
@@ -217,8 +201,6 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : poly:bool -> hints_expr -> hints_entry
-
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable
new file mode 100644
index 0000000000..ffaa7e70f4
--- /dev/null
+++ b/vernac/.ocamlformat-enable
@@ -0,0 +1 @@
+comHints.ml
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 9698c14452..f410cddfef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
     Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
     when said type is not a registered type class. *)
 
-val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val new_instance_interactive
@@ -34,7 +34,7 @@ val new_instance_interactive
   -> ?generalize:bool
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
-  -> Hints.hint_info_expr
+  -> ComHints.hint_info_expr
   -> (bool * constr_expr) option
   -> Id.t * Lemmas.t
 
@@ -47,7 +47,7 @@ val new_instance
   -> (bool * constr_expr)
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> Hints.hint_info_expr
+  -> ComHints.hint_info_expr
   -> Id.t
 
 val new_instance_program
@@ -59,7 +59,7 @@ val new_instance_program
   -> (bool * constr_expr) option
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> Hints.hint_info_expr
+  -> ComHints.hint_info_expr
   -> Id.t
 
 val declare_new_instance
@@ -69,7 +69,7 @@ val declare_new_instance
   -> ident_decl
   -> local_binder_expr list
   -> constr_expr
-  -> Hints.hint_info_expr
+  -> ComHints.hint_info_expr
   -> unit
 
 (** {6 Low level interface used by Add Morphism, do not use } *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
new file mode 100644
index 0000000000..324fee72ec
--- /dev/null
+++ b/vernac/comHints.ml
@@ -0,0 +1,174 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+
+(** (Partial) implementation of the [Hint] command; some more
+   functionality still lives in tactics/hints.ml *)
+
+type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
+
+type reference_or_constr =
+  | HintsReference of Libnames.qualid
+  | HintsConstr of Constrexpr.constr_expr
+
+type hints_expr =
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolveIFF of bool * Libnames.qualid list * int option
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.qualid list
+  | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
+  | HintsMode of Libnames.qualid * Hints.hint_mode list
+  | HintsConstructors of Libnames.qualid list
+  | HintsExtern of
+      int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
+let project_hint ~poly pri l2r r =
+  let open EConstr in
+  let open Coqlib in
+  let gr = Smartlocate.global_with_alias r in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, c = Evd.fresh_global env sigma gr in
+  let t = Retyping.get_type_of env sigma c in
+  let t =
+    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t
+  in
+  let sign, ccl = decompose_prod_assum sigma t in
+  let a, b =
+    match snd (decompose_app sigma ccl) with
+    | [a; b] -> (a, b)
+    | _ -> assert false
+  in
+  let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let c =
+    Reductionops.whd_beta sigma
+      (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
+  in
+  let c =
+    it_mkLambda_or_LetIn
+      (mkApp
+         ( p
+         , [| mkArrow a Sorts.Relevant (Vars.lift 1 b)
+            ; mkArrow b Sorts.Relevant (Vars.lift 1 a)
+            ; c |] ))
+      sign
+  in
+  let name =
+    Nameops.add_suffix
+      (Nametab.basename_of_global gr)
+      ("_proj_" ^ if l2r then "l2r" else "r2l")
+  in
+  let ctx = Evd.univ_entry ~poly sigma in
+  let c = EConstr.to_constr sigma c in
+  let cb =
+    Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
+  in
+  let c =
+    Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+      ~kind:Decls.(IsDefinition Definition)
+      cb
+  in
+  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+  (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
+
+let warn_deprecated_hint_constr =
+  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+    (fun () ->
+      Pp.strbrk
+        "Declaring arbitrary terms as hints is deprecated; declare a global \
+         reference instead")
+
+let interp_hints ~poly h =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let f poly c =
+    let evd, c = Constrintern.interp_open_constr env sigma c in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let c, diff = Hints.prepare_hint true env sigma (evd, c) in
+    if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
+    else
+      let () = Declare.declare_universe_context ~poly:false diff in
+      (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
+  in
+  let fref r =
+    let gr = Smartlocate.global_with_alias r in
+    Dumpglob.add_glob ?loc:r.CAst.loc gr;
+    gr
+  in
+  let fr r = Tacred.evaluable_of_global_reference env (fref r) in
+  let fi c =
+    let open Hints in
+    match c with
+    | HintsReference c ->
+      let gr = Smartlocate.global_with_alias c in
+      (PathHints [gr], poly, IsGlobRef gr)
+    | HintsConstr c ->
+      let () = warn_deprecated_hint_constr () in
+      (PathAny, poly, f poly c)
+  in
+  let fp = Constrintern.intern_constr_pattern env sigma in
+  let fres (info, b, r) =
+    let path, poly, gr = fi r in
+    let info =
+      { info with
+        Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern
+      }
+    in
+    (info, poly, b, path, gr)
+  in
+  let ft =
+    let open Hints in
+    function
+    | HintsVariables -> HintsVariables
+    | HintsConstants -> HintsConstants
+    | HintsReferences lhints -> HintsReferences (List.map fr lhints)
+  in
+  let fp = Constrintern.intern_constr_pattern (Global.env ()) in
+  let open Hints in
+  match h with
+  | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
+  | HintsResolveIFF (l2r, lc, n) ->
+    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
+  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
+  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
+  | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
+  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
+  | HintsConstructors lqid ->
+    let constr_hints_of_ind qid =
+      let ind = Smartlocate.global_inductive_with_alias qid in
+      let mib, _ = Global.lookup_inductive ind in
+      Dumpglob.dump_reference ?loc:qid.CAst.loc "<>"
+        (Libnames.string_of_qualid qid)
+        "ind";
+      List.init (Inductiveops.nconstructors env ind) (fun i ->
+          let c = (ind, i + 1) in
+          let gr = Names.GlobRef.ConstructRef c in
+          ( empty_hint_info
+          , Declareops.inductive_is_polymorphic mib
+          , true
+          , PathHints [gr]
+          , IsGlobRef gr ))
+    in
+    HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
+  | HintsExtern (pri, patcom, tacexp) ->
+    let pat = Option.map (fp sigma) patcom in
+    let l = match pat with None -> [] | Some (l, _) -> l in
+    let ltacvars =
+      List.fold_left
+        (fun accu x -> Names.Id.Set.add x accu)
+        Names.Id.Set.empty l
+    in
+    let env = Genintern.{(empty_glob_sign env) with ltacvars} in
+    let _, tacexp = Genintern.generic_intern env tacexp in
+    HintsExternEntry
+      ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp)
diff --git a/vernac/comHints.mli b/vernac/comHints.mli
new file mode 100644
index 0000000000..77fbef5387
--- /dev/null
+++ b/vernac/comHints.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Typeclasses
+
+type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
+
+type reference_or_constr =
+  | HintsReference of Libnames.qualid
+  | HintsConstr of Constrexpr.constr_expr
+
+type hints_expr =
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolveIFF of bool * Libnames.qualid list * int option
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.qualid list
+  | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
+  | HintsMode of Libnames.qualid * Hints.hint_mode list
+  | HintsConstructors of Libnames.qualid list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
+val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 058fa691ee..e84fce5504 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,6 +14,7 @@ open Glob_term
 open Constrexpr
 open Vernacexpr
 open Hints
+open ComHints
 
 open Pcoq
 open Pcoq.Prim
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 36d79bfdb1..f1aae239aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -185,7 +185,7 @@ open Pputils
     | [] -> mt()
     | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
-  let pr_reference_or_constr pr_c = let open Hints in function
+  let pr_reference_or_constr pr_c = let open ComHints in function
     | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
@@ -202,6 +202,7 @@ open Pputils
     let opth = pr_opt_hintbases db  in
     let pph =
       let open Hints in
+      let open ComHints in
       match h with
         | HintsResolve l ->
           keyword "Resolve " ++ prlist_with_sep sep
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4de12f5e3b..2b6beaf2e3 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -28,7 +28,7 @@ module Vernac_ :
     val command_entry : vernac_expr Entry.t
     val main_entry : vernac_control option Entry.t
     val red_expr : raw_red_expr Entry.t
-    val hint_info : Hints.hint_info_expr Entry.t
+    val hint_info : ComHints.hint_info_expr Entry.t
   end
 
 (* To be removed when the parser is made functional wrt the tactic
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index b7728fe699..3d3be8050d 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,6 +9,7 @@ Himsg
 Locality
 Egramml
 Vernacextend
+ComHints
 Ppvernac
 Proof_using
 Egramcoq
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3926b91a55..028a7d0859 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1275,7 +1275,7 @@ let vernac_hints ~atts dbnames h =
       "This command does not support the export attribute in sections.");
   | OptDefault | OptLocal -> ()
   in
-  Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
+  Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index e46186288e..b65a0da1cc 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -336,18 +336,18 @@ type nonrec vernac_expr =
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
       (bool * constr_expr) option * (* body (bool=true when using {}) *)
-      Hints.hint_info_expr
+      ComHints.hint_info_expr
 
   | VernacDeclareInstance of
       ident_decl * (* name *)
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
-      Hints.hint_info_expr
+      ComHints.hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacExistingInstance of
-    (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+    (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacExistingClass of qualid (* inductive or definition name *)
 
@@ -387,7 +387,7 @@ type nonrec vernac_expr =
   (* Commands *)
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * qualid list
-  | VernacHints of string list * Hints.hints_expr
+  | VernacHints of string list * ComHints.hints_expr
   | VernacSyntacticDefinition of
       lident * (Id.t list * constr_expr) *
       onlyparsing_flag