From 8e861557feb58d6ee45b2c67c8191092fef9ec6a Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 16 Jan 2003 17:21:38 +0000
Subject: Subst sur une hyp qui n'existe pas ne fait pas une anomalie

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5bf7451217..dbff4f520b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1174,7 +1174,7 @@ let eq_rhs eq =
 
 let subst_one x gl = 
   let hyps = pf_hyps gl in
-  let (_,xval,_) = Sign.lookup_named x hyps in
+  let (_,xval,_) = pf_get_hyp gl x in
   (* If x has a body, simply replace x with body and clear x *)
   if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
   (* x is a variable: *)
-- 
cgit v1.2.3