From b0abddeb3e466e7e33c5d94f2421bcc7c131469b Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 8 Oct 2002 15:32:58 +0000
Subject: Subst ne fait pas clear sur x:=e

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index da35ef0d1c..1b376a92c7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1223,6 +1223,7 @@ let subst_one x gl =
     in
     map_succeed test hyps
   in
+  let clear_x = let (_,d,_) = Sign.lookup_named x (pf_hyps gl) in d = None in
   let dephyps = List.rev dephyps in
   tclTHENLIST [
     generalize (List.map mkVar dephyps);
@@ -1230,7 +1231,7 @@ let subst_one x gl =
     rewriteLR (mkVar hyp);
     intros_using dephyps;
     clear [hyp];
-    tclTRY (clear [x])
+    if clear_x then tclTRY (clear [x]) else tclIDTAC
   ] gl
 
 let rec subst = function
-- 
cgit v1.2.3