Move evaluable_global_reference from Names to Tacred.

It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.

In any case this type does not belong to the kernel.

5 files changed, 7 insertions, 4 deletions

diff --git a/vernac/classes.mli b/vernac/classes.mli
index e1816fb138..89ff4e6939 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -81,7 +81,7 @@ val add_class : env -> Evd.evar_map -> typeclass -> unit
 
 (** Setting opacity *)
 
-val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
+val set_typeclass_transparency : Tacred.evaluable_global_reference -> bool -> bool -> unit
 
 (** For generation on names based on classes only *)
 
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index f642411fa4..1c36e10e83 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -76,6 +76,7 @@ let warn_deprecated_hint_constr =
  *)
 let soft_evaluable =
   let open GlobRef in
+  let open Tacred in
   function
   | ConstRef c -> EvalConstRef c
   | VarRef id -> EvalVarRef id
diff --git a/vernac/declare.ml b/vernac/declare.ml
index fafee13bf6..c715304419 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -883,7 +883,7 @@ let shrink_body c ty =
 (* Saving an obligation                                                *)
 (***********************************************************************)
 
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+let unfold_entry cst = Hints.HintsUnfoldEntry [Tacred.EvalConstRef cst]
 
 let add_hint local prg cst =
   let locality = if local then Goptions.OptLocal else Goptions.OptExport in
diff --git a/vernac/record.ml b/vernac/record.ml
index 583164a524..68219603b4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -625,7 +625,7 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind
   let cref = GlobRef.ConstRef cst in
   Impargs.declare_manual_implicits false cref paramimpls;
   Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs);
-  Classes.set_typeclass_transparency (EvalConstRef cst) false false;
+  Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false;
   let sub = List.hd coers in
   let m = {
     meth_name = Name proj_name;
@@ -744,7 +744,7 @@ let add_constant_class env sigma cst =
     }
   in
   Classes.add_class env sigma tc;
-    Classes.set_typeclass_transparency (EvalConstRef cst) false false
+    Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false
 
 let add_inductive_class env sigma ind =
   let mind, oneind = Inductive.lookup_mind_specif env ind in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a3726daf63..e8cb1d65a9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1628,6 +1628,7 @@ let () =
     }
 
 let vernac_set_strategy ~local l =
+  let open Tacred in
   let local = Option.default false local in
   let glob_ref r =
     match smart_global r with
@@ -1639,6 +1640,7 @@ let vernac_set_strategy ~local l =
   Redexpr.set_strategy local l
 
 let vernac_set_opacity ~local (v,l) =
+  let open Tacred in
   let local = Option.default true local in
   let glob_ref r =
     match smart_global r with