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.

36 files changed, 90 insertions, 84 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 2aeb1ea202..4778bf1121 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -340,15 +340,6 @@ let subst_retro_action subst action =
     let c' = subst_constant subst c in
     if c == c' then action else Register_type(prim, c')
 
-(* Here the semantics is completely unclear.
-   What does "Hint Unfold t" means when "t" is a parameter?
-   Does the user mean "Unfold X.t" or does she mean "Unfold y"
-   where X.t is later on instantiated with y? I choose the first
-   interpretation (i.e. an evaluable reference is never expanded). *)
-let subst_evaluable_reference subst = function
-  | EvalVarRef id -> EvalVarRef id
-  | EvalConstRef kn -> EvalConstRef (subst_constant subst kn)
-
 let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind c with
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index bc5816dafb..9cf270cff7 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -146,14 +146,6 @@ val subst_proj : substitution -> Projection.t -> Projection.t
 
 val subst_retro_action : substitution -> Retroknowledge.action -> Retroknowledge.action
 
-(** Here the semantics is completely unclear.
-   What does "Hint Unfold t" means when "t" is a parameter?
-   Does the user mean "Unfold X.t" or does she mean "Unfold y"
-   where X.t is later on instantiated with y? I choose the first
-   interpretation (i.e. an evaluable reference is never expanded). *)
-val subst_evaluable_reference :
-  substitution -> evaluable_global_reference -> evaluable_global_reference
-
 (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
 val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
 
diff --git a/kernel/names.ml b/kernel/names.ml
index be65faf234..60c6c7bd67 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1100,16 +1100,6 @@ module GlobRef = struct
 
 end
 
-type evaluable_global_reference =
-  | EvalVarRef of Id.t
-  | EvalConstRef of Constant.t
-
-(* Better to have it here that in closure, since used in grammar.cma *)
-let eq_egr e1 e2 = match e1, e2 with
-    EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
-  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
-  | _, _ -> false
-
 (** Located identifiers and objects with syntax. *)
 
 type lident = Id.t CAst.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 747299bb12..09885396c0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -714,14 +714,6 @@ module GlobRef : sig
 
 end
 
-(** Better to have it here that in Closure, since required in grammar.cma *)
-(* XXX: Move to a module *)
-type evaluable_global_reference =
-  | EvalVarRef of Id.t
-  | EvalConstRef of Constant.t
-
-val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
-
 (** Located identifiers and objects with syntax. *)
 
 type lident = Id.t CAst.t
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 73eb943418..67b6839b6e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
                       tclTHENLIST
                         [ unfold_in_concl
                             [ ( Locus.AllOccurrences
-                              , Names.EvalConstRef (fst fname) ) ]
+                              , Tacred.EvalConstRef (fst fname) ) ]
                         ; (let do_prove =
                              build_proof interactive_proof
                                (Array.to_list fnames)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 314c8abcaf..c344fdd611 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -917,13 +917,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
             tclTHENLIST
               [ unfold_in_concl
                   [ ( Locus.AllOccurrences
-                    , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+                    , Tacred.EvalVarRef (destVar sigma args.(1)) ) ]
               ; tclMAP
                   (fun id ->
                     tclTRY
                       (unfold_in_hyp
                          [ ( Locus.AllOccurrences
-                           , Names.EvalVarRef (destVar sigma args.(1)) ) ]
+                           , Tacred.EvalVarRef (destVar sigma args.(1)) ) ]
                          (destVar sigma args.(1), Locus.InHyp)))
                   (pf_ids_of_hyps g)
               ; intros_with_rewrite () ]
@@ -936,13 +936,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic =
             tclTHENLIST
               [ unfold_in_concl
                   [ ( Locus.AllOccurrences
-                    , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+                    , Tacred.EvalVarRef (destVar sigma args.(2)) ) ]
               ; tclMAP
                   (fun id ->
                     tclTRY
                       (unfold_in_hyp
                          [ ( Locus.AllOccurrences
-                           , Names.EvalVarRef (destVar sigma args.(2)) ) ]
+                           , Tacred.EvalVarRef (destVar sigma args.(2)) ) ]
                          (destVar sigma args.(2), Locus.InHyp)))
                   (pf_ids_of_hyps g)
               ; intros_with_rewrite () ]
@@ -1158,7 +1158,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i :
             else
               unfold_in_concl
                 [ ( Locus.AllOccurrences
-                  , Names.EvalConstRef
+                  , Tacred.EvalConstRef
                       (fst (destConst (Proofview.Goal.sigma g) f)) ) ]
           in
           (* The proof of each branche itself *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6464556e4e..266345a324 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -418,6 +418,7 @@ let make_eq () =
   with _ -> assert false
 
 let evaluable_of_global_reference r =
+  let open Tacred in
   (* Tacred.evaluable_of_global_reference (Global.env ()) *)
   match r with
   | GlobRef.ConstRef sp -> EvalConstRef sp
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7b7044fdaf..e25f413fe4 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -100,7 +100,7 @@ val acc_rel : EConstr.constr Util.delayed
 val well_founded : EConstr.constr Util.delayed
 
 val evaluable_of_global_reference :
-  GlobRef.t -> Names.evaluable_global_reference
+  GlobRef.t -> Tacred.evaluable_global_reference
 
 val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index faad792ea9..6ebb01703f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -191,8 +191,8 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_and_short_name pr (c,_) = pr c
 
   let pr_evaluable_reference = function
-    | EvalVarRef id -> pr_id id
-    | EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
+    | Tacred.EvalVarRef id -> pr_id id
+    | Tacred.EvalConstRef sp -> pr_global (GlobRef.ConstRef sp)
 
   let pr_quantified_hypothesis = function
     | AnonHyp n -> int n
@@ -381,8 +381,8 @@ let string_of_genarg_arg (ArgumentType arg) =
         str "<" ++ KerName.print kn ++ str ">"
 
   let pr_evaluable_reference_env env = function
-    | EvalVarRef id -> pr_id id
-    | EvalConstRef sp ->
+    | Tacred.EvalVarRef id -> pr_id id
+    | Tacred.EvalConstRef sp ->
       Nametab.pr_global_env (Termops.vars_of_env env) (GlobRef.ConstRef sp)
 
   let pr_as_disjunctive_ipat prc ipatl =
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 79e0adf9f7..4f58eceb59 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -106,7 +106,7 @@ val pr_may_eval :
 
 val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
 
-val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
+val pr_evaluable_reference_env : env -> Tacred.evaluable_global_reference -> Pp.t
 
 val pr_quantified_hypothesis : quantified_hypothesis -> Pp.t
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 9abdc2ddbe..5e88bf7c79 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -276,6 +276,7 @@ let coerce_to_closed_constr env v =
   c
 
 let coerce_to_evaluable_ref env sigma v =
+  let open Tacred in
   let fail () = raise (CannotCoerceTo "an evaluable reference") in
   let ev =
   match is_intro_pattern v with
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index b8592c5c76..8ca2510459 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -69,7 +69,7 @@ val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
 val coerce_to_evaluable_ref :
-  Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference
+  Environ.env -> Evd.evar_map -> Value.t -> Tacred.evaluable_global_reference
 
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 7b2c8e1d04..a880a3305e 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -270,7 +270,7 @@ constraint 'a = <
 
 type g_trm = Genintern.glob_constr_and_expr
 type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
+type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
@@ -324,7 +324,7 @@ type raw_tactic_arg =
 
 type t_trm = EConstr.constr
 type t_pat = constr_pattern
-type t_cst = evaluable_global_reference
+type t_cst = Tacred.evaluable_global_reference
 type t_ref = ltac_constant located
 type t_nam = Id.t
 
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 2382dcfbb9..3bb20b9d19 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -269,7 +269,7 @@ constraint 'a = <
 
 type g_trm = Genintern.glob_constr_and_expr
 type g_pat = Genintern.glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference Genredexpr.and_short_name or_var
+type g_cst = Tacred.evaluable_global_reference Genredexpr.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
@@ -323,7 +323,7 @@ type raw_tactic_arg =
 
 type t_trm = EConstr.constr
 type t_pat = constr_pattern
-type t_cst = evaluable_global_reference
+type t_cst = Tacred.evaluable_global_reference
 type t_ref = ltac_constant located
 type t_nam = Id.t
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 8bee7afa2c..ae7a10ce52 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -308,8 +308,8 @@ let short_name qid =
   else None
 
 let evalref_of_globref ?loc ?short = function
-  | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
-  | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+  | GlobRef.ConstRef cst -> ArgArg (Tacred.EvalConstRef cst, short)
+  | GlobRef.VarRef id -> ArgArg (Tacred.EvalVarRef id, short)
   | r ->
     let tpe = match r with
     | GlobRef.IndRef _ -> "inductive"
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 90546ea939..6148f0d23f 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -89,7 +89,7 @@ let subst_global_reference subst =
   Locusops.or_var_map (subst_located (subst_global_reference subst))
 
 let subst_evaluable subst =
-  let subst_eval_ref = subst_evaluable_reference subst in
+  let subst_eval_ref = Tacred.subst_evaluable_reference subst in
     Locusops.or_var_map (subst_and_short_name subst_eval_ref)
 
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index a7b571d3db..7d959aa788 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -189,6 +189,7 @@ let flatten_contravariant_disj _ ist =
   | _ -> fail
 
 let evalglobref_of_globref =
+  let open Tacred in
   function
   | GlobRef.VarRef v -> EvalVarRef v
   | GlobRef.ConstRef c -> EvalConstRef c
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4f7b3fbe74..9d92ffde74 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -354,8 +354,9 @@ let coq_True = gen_constant "core.True.type"
 let evaluable_ref_of_constr s c =
   let env = Global.env () in
   let evd = Evd.from_env env in
+  let open Tacred in
   match EConstr.kind evd (Lazy.force c) with
-  | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
+  | Const (kn,u) when is_evaluable env (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index fdfba48024..723c786b4f 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -223,11 +223,11 @@ let simplintac occ rdx sim =
   end
 
 let rec get_evalref env sigma c = match EConstr.kind sigma c with
-  | Var id -> EvalVarRef id
-  | Const (k,_) -> EvalConstRef k
+  | Var id -> Tacred.EvalVarRef id
+  | Const (k,_) -> Tacred.EvalConstRef k
   | App (c', _) -> get_evalref env sigma c'
   | Cast (c', _, _) -> get_evalref env sigma c'
-  | Proj(c,_) -> EvalConstRef(Projection.constant c)
+  | Proj(c,_) -> Tacred.EvalConstRef(Projection.constant c)
   | _ -> errorstrm Pp.(str "The term " ++ pr_econstr_pat (Global.env ()) sigma c ++ str " is not unfoldable")
 
 (* Strip a pattern generated by a prenex implicit to its constant. *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c705ac16e7..411fb0cd89 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -43,6 +43,25 @@ exception ReductionTacticError of reduction_tactic_error
 exception Elimconst
 exception Redelimination
 
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+(* Better to have it here that in closure, since used in grammar.cma *)
+let eq_egr e1 e2 = match e1, e2 with
+    EvalConstRef con1, EvalConstRef con2 -> Constant.CanOrd.equal con1 con2
+  | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
+  | _, _ -> false
+
+(* Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
+let subst_evaluable_reference subst = function
+  | EvalVarRef id -> EvalVarRef id
+  | EvalConstRef kn -> EvalConstRef (Mod_subst.subst_constant subst kn)
+
 let error_not_evaluable r =
   user_err ~hdr:"error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 65e3421736..aa232175bb 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -18,6 +18,21 @@ open Locus
 open Univ
 open Ltac_pretype
 
+(* XXX: Move to a module *)
+type evaluable_global_reference =
+  | EvalVarRef of Id.t
+  | EvalConstRef of Constant.t
+
+val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
+
+(** Here the semantics is completely unclear.
+   What does "Hint Unfold t" means when "t" is a parameter?
+   Does the user mean "Unfold X.t" or does she mean "Unfold y"
+   where X.t is later on instantiated with y? I choose the first
+   interpretation (i.e. an evaluable reference is never expanded). *)
+val subst_evaluable_reference :
+  Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_reference
+
 type reduction_tactic_error =
     InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 732af5570d..524c715455 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -154,7 +154,7 @@ val pr_existential_key     : evar_map -> Evar.t -> Pp.t
 val pr_existential         : env -> evar_map -> existential -> Pp.t
 val pr_constructor         : env -> constructor -> Pp.t
 val pr_inductive           : env -> inductive -> Pp.t
-val pr_evaluable_reference : evaluable_global_reference -> Pp.t
+val pr_evaluable_reference : Tacred.evaluable_global_reference -> Pp.t
 
 val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
 val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 08f88d46c1..6a6dd783e4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -69,7 +69,7 @@ val pf_reduce_to_atomic_ind     : Goal.goal sigma -> types -> (inductive * EInst
 [@@ocaml.deprecated "Use Tacred.pf_reduce_to_atomic_ind"]
 val pf_compute                 : Goal.goal sigma -> constr -> constr
 [@@ocaml.deprecated "Use the version in Tacmach.New"]
-val pf_unfoldn    : (occurrences * evaluable_global_reference) list
+val pf_unfoldn    : (occurrences * Tacred.evaluable_global_reference) list
   -> Goal.goal sigma -> constr -> constr
 [@@ocaml.deprecated "Use Tacred.unfoldn"]
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 369508c2a3..353e138599 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -277,8 +277,8 @@ let hintmap_of env sigma secvars hdc concl =
      else Hint_db.map_auto env sigma ~secvars hdc concl
 
 let exists_evaluable_reference env = function
-  | EvalConstRef _ -> true
-  | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
+  | Tacred.EvalConstRef _ -> true
+  | Tacred.EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false
 
 let dbg_intro dbg = tclLOG dbg (fun _ _ -> str "intro") intro
 let dbg_assumption dbg = tclLOG dbg (fun _ _ -> str "assumption") assumption
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e920093648..20c557b282 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -386,6 +386,7 @@ let make_dimension n = function
   | Some d -> (false,d)
 
 let autounfolds ids csts gl cls =
+  let open Tacred in
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
   let env = Tacmach.New.pf_env gl in
   let ids = List.filter (fun id -> List.mem id hyps && Tacred.is_evaluable env (EvalVarRef id)) ids in
diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
index 9939490e79..a9100efddb 100644
--- a/tactics/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -76,7 +76,7 @@ type 'a and_short_name = 'a * Names.lident option
 
 let wit_red_expr :
   ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
-   (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
-   (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
+   (Genintern.glob_constr_and_expr,Tacred.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
+   (EConstr.t,Tacred.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
     Genarg.genarg_type =
   make0 "redexpr"
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 54f4716652..f5947bb946 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -36,7 +36,7 @@ type 'a hint_ast =
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
-  | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
+  | Unfold_nth of Tacred.evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Pattern.constr_pattern option * Genarg.glob_generic_argument       (* Hint Extern *)
 
 type hint = private {
@@ -173,8 +173,8 @@ type hints_entry =
   | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * hint_term) list
   | HintsCutEntry of hints_path
-  | HintsUnfoldEntry of evaluable_global_reference list
-  | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
+  | HintsUnfoldEntry of Tacred.evaluable_global_reference list
+  | HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool
   | HintsModeEntry of GlobRef.t * hint_mode list
   | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 9c2df71f82..b415b30de8 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -81,7 +81,7 @@ let subst_strategy (subs,(local,obj)) =
   local,
   List.Smart.map
     (fun (k,ql as entry) ->
-      let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
+      let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in
       if ql==ql' then entry else (k,ql'))
     obj
 
@@ -344,7 +344,7 @@ let subst_red_expr subs =
   let sigma = Evd.from_env env in
   Redops.map_red_expr_gen
     (subst_mps subs)
-    (Mod_subst.subst_evaluable_reference subs)
+    (Tacred.subst_evaluable_reference subs)
     (Patternops.subst_pattern env sigma subs)
 
 let inReduction : bool * string * red_expr -> obj =
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
index 5f3a7b689b..fb0043db8d 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -10,7 +10,6 @@
 
 (** Interpretation layer of redexprs such as hnf, cbv, etc. *)
 
-open Names
 open Constr
 open EConstr
 open Pattern
@@ -19,7 +18,7 @@ open Reductionops
 open Locus
 
 type red_expr =
-  (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+  (constr, Tacred.evaluable_global_reference, constr_pattern) red_expr_gen
 
 type red_expr_val
 
@@ -50,7 +49,7 @@ val declare_red_expr : bool -> string -> red_expr -> unit
    true, the effect is non-synchronous (i.e. it does not survive
    section and module closure). *)
 val set_strategy :
-  bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
+  bool -> (Conv_oracle.level * Tacred.evaluable_global_reference list) list -> unit
 
 (** call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0fd2f1253f..a6471be549 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -179,11 +179,11 @@ val normalise_in_hyp  : hyp_location -> unit Proofview.tactic
 val normalise_option  : goal_location -> unit Proofview.tactic
 val normalise_vm_in_concl : unit Proofview.tactic
 val unfold_in_concl   :
-  (occurrences * evaluable_global_reference) list -> unit Proofview.tactic
+  (occurrences * Tacred.evaluable_global_reference) list -> unit Proofview.tactic
 val unfold_in_hyp     :
-  (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic
+  (occurrences * Tacred.evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic
 val unfold_option     :
-  (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
+  (occurrences * Tacred.evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
   check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
 val pattern_option    :
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 69758b3f37..54f5a2cf68 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -209,13 +209,13 @@ let letin_pat_tac ev ipat na c cl =
     Instead, we parse indifferently any pattern and dispatch when the tactic is
     called. *)
 let map_pattern_with_occs (pat, occ) = match pat with
-| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst))
-| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id))
+| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (Tacred.EvalConstRef cst))
+| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (Tacred.EvalVarRef id))
 | _ -> (mk_occurrences_expr occ, Inr pat)
 
 let get_evaluable_reference = function
-| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id)
-| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst)
+| GlobRef.VarRef id -> Proofview.tclUNIT (Tacred.EvalVarRef id)
+| GlobRef.ConstRef cst -> Proofview.tclUNIT (Tacred.EvalConstRef cst)
 | r ->
   Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++
     Nametab.pr_global_env Id.Set.empty r ++ spc () ++
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