From 1d6edcfa1b5969f082572d2b083b8160c2385bcd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Oct 2003 12:47:19 +0000
Subject: Bug Double Inversion

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

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 4cb44c31ec..e3235fc32a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -169,7 +169,8 @@ let induction_trailer abs_i abs_j bargs =
 	  in
           let ids = List.rev (ids_of_named_context hyps) in
 	  (tclTHENSEQ
-            [bring_hyps hyps; clear ids; simple_elimination (mkVar id)])
+            [bring_hyps hyps; tclTRY (clear ids); 
+	     simple_elimination (mkVar id)])
           gls))
 
 let double_ind h1 h2 gls =
-- 
cgit v1.2.3