Merge PR #13321: Move evaluable_global_reference from Names to Tacred.

Reviewed-by: herbelin
Ack-by: ejgallego

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 aeb6b3cf85..0008d31ffd 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. *)