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.

15 files changed, 28 insertions, 24 deletions

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. *)