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    :