From 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 29 Oct 2020 13:59:45 +0100
Subject: 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.
---
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/gen_principle.ml                | 10 +++++-----
 plugins/funind/indfun_common.ml                |  1 +
 plugins/funind/indfun_common.mli               |  2 +-
 4 files changed, 8 insertions(+), 7 deletions(-)

(limited to 'plugins/funind')

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
 
-- 
cgit v1.2.3