From dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 31 Oct 2013 14:24:43 +0000
Subject: Conv_orable made functional and part of pre_env

But for vm, the kernel should be functional now

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml | 4 ++--
 tactics/tactics.ml | 5 +++--
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index eb7b28690b..d6ad598c5b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1048,8 +1048,8 @@ module Strategies =
 	lemmas rewrite_unif_flags lems state env avoid t ty cstr evars
 
     let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
-      let rfn, ckind = Redexpr.reduction_of_red_expr r in
-	fun state env avoid t ty cstr evars ->
+      fun state env avoid t ty cstr evars ->
+        let rfn, ckind = Redexpr.reduction_of_red_expr env r in
 	  let t' = rfn env (goalevars evars) t in
 	    if eq_constr t' t then
 	      state, Some None
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c1bd8e0c97..004a93ed18 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -379,7 +379,8 @@ let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
   let tac = tclMAP (fun (where,redexp) ->
-    reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in
+    reduct_option
+      (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
   match redexp with
   | Fold _ | Pattern _ -> with_check tac goal
   | _ -> tac goal
@@ -552,7 +553,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
           aux
-	    ((fst (Redexpr.reduction_of_red_expr (Red true)))
+	    ((fst (Redexpr.reduction_of_red_expr env (Red true)))
 	       env (project gl) ccl)
       | x -> x
   in
-- 
cgit v1.2.3