From 077502620d56a33604b9dfaf0a214516e0d780a2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 10:36:04 +0000
Subject: Un Try supplementaire utile pour la compatibilite, car bring_hyps
 dans generalizeRewriteIntros peut echouer (typage)

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

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0ffe210674..6033ffa233 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -314,9 +314,7 @@ let projectAndApply thin id eqname names depids gls =
     match (kind_of_term t1, kind_of_term t2) with
       | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
       | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
-      | _ ->
-	  
-	  tac id gls
+      | _ -> tac id gls
   in
   let deq_trailer id neqns =
     tclTHENSEQ 
@@ -325,8 +323,8 @@ let projectAndApply thin id eqname names depids gls =
 	 tclTHEN
 	   (intro_move idopt None)
 	   (* try again to substitute and if still not a variable after *)
-	   (* decomposition, arbitraryly try to rewrite RL !? *)
-	   (onLastHyp (substHypIfVariable subst_hyp_RL)))
+	   (* decomposition, arbitrarily try to rewrite RL !? *)
+	   (tclTRY (onLastHyp (substHypIfVariable subst_hyp_RL))))
 	 names);
        (if names = [] then clear [id] else tclIDTAC)]
   in
-- 
cgit v1.2.3