From 7343f5ca64222d536656025eab36d2592693437e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 May 2004 16:33:38 +0000
Subject: Bug mauvais sigma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5735 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 989944ae99..5a8a0c81bc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -332,7 +332,8 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
   let env = pf_env gl in
   let rec aux ccl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
-      | None when red -> aux (reduction_of_redexp (Red true) env Evd.empty ccl)
+      | None when red ->
+          aux (reduction_of_redexp (Red true) env (project gl) ccl)
       | x -> x
   in
   try aux (pf_concl gl)
-- 
cgit v1.2.3