From 7b5e9f8cc06b047a5abbb9b0d93af25d68f4a2ac Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 5 Mar 2002 16:48:51 +0000
Subject: *** empty log message ***

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

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 63c6eac3e2..07466c4975 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -267,15 +267,12 @@ let projectAndApply thin id depids gls =
           (tclTHEN (subst_hyp_RL id) (clear [id])) depids id2 gls
     | (false, _ , Var id2) ->
         generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
-    | (true, _, _) ->
+    | _ ->
+        let trailer =
+          if thin then onLastHyp (fun id -> clear [id]) else tclIDTAC in
         let deq_trailer neqns =
           tclDO neqns
-            (tclTHENSEQ
-              [intro; subst_hyp; onLastHyp (fun id -> clear [id])])
-        in 
-	(tclTHEN (tclTRY (dEqThen deq_trailer (Some id))) (clear [id])) gls
-    | (false, _, _) -> 
-        let deq_trailer neqns = tclDO neqns (tclTHEN intro subst_hyp) in 
+            (tclTHENSEQ [intro; tclTRY subst_hyp; trailer]) in 
 	(tclTHEN (dEqThen deq_trailer (Some id)) (clear [id])) gls
 
 (* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
-- 
cgit v1.2.3