diff options
| author | barras | 2002-03-05 16:48:51 +0000 |
|---|---|---|
| committer | barras | 2002-03-05 16:48:51 +0000 |
| commit | 7b5e9f8cc06b047a5abbb9b0d93af25d68f4a2ac (patch) | |
| tree | 94431a657c3d010d7036205258233834a862063d | |
| parent | c877c64b4592d77c28c7932f73d4bb98142116b2 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2516 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/inv.ml | 11 |
1 files 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 |