Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dans redexpr.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 6 insertions, 6 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index ddfb9bd12a..f5b35e57db 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -94,7 +94,7 @@ val h_simplest_right  : tactic
 
 
 (* Conversion *)
-val h_reduce          : Tacred.red_expr -> Tacticals.clause -> tactic
+val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
   constr occurrences option -> constr -> Tacticals.clause -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a4360e5ea6..8eb7982125 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1242,7 +1242,7 @@ let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
 let interp_may_eval f ist gl = function
   | ConstrEval (r,c) ->
       let redexp = pf_redexp_interp ist gl  r in
-      pf_reduction_of_redexp gl redexp (f ist gl c)
+      pf_reduction_of_red_expr gl redexp (f ist gl c)
   | ConstrContext ((loc,s),c) ->
       (try
 	let ic = f ist gl c
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 8d8d12fb40..2173b058c7 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -105,7 +105,7 @@ val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
 
 (* Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr
-  -> Tacred.red_expr
+  -> Redexpr.red_expr
 
 (* Interprets tactic expressions *)
 val interp_tac_gen : (identifier * value) list -> 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 872baa1799..bc91ddb3ec 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -226,7 +226,7 @@ let pattern_option l = reduct_option (pattern_occs l)
    as the command Eval does. *)
 
 let reduce redexp cl goal =
-  redin_combinator (reduction_of_redexp redexp) cl goal
+  redin_combinator (Redexpr.reduction_of_red_expr redexp) cl goal
 
 (* Unfolding occurrences of a constant *)
 
@@ -338,7 +338,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
   let rec aux ccl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
-          aux (reduction_of_redexp (Red true) env (project gl) ccl)
+          aux (Redexpr.reduction_of_red_expr (Red true) env (project gl) ccl)
       | x -> x
   in
   try aux (pf_concl gl)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a6b906b34d..418c3095f7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -19,7 +19,7 @@ open Reduction
 open Evd
 open Evar_refiner
 open Clenv
-open Tacred
+open Redexpr
 open Tacticals
 open Libnames
 open Genarg