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.

7 files changed, 15 insertions, 15 deletions

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    :