diff options
| author | herbelin | 2011-04-24 08:59:18 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-24 08:59:18 +0000 |
| commit | ef6bddfdcf87d90e9ad7f682cfa5e24a1a53f3c5 (patch) | |
| tree | de3cf491556c49d9f82b80f2f224729b9a13d2b2 /tactics | |
| parent | c250c03254bda83775647b47bc35274ea0747647 (diff) | |
Fixed a bug of destruct which was sometimes forgetting local definitions behind it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14053 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f259dd9213..336be31d89 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1737,6 +1737,9 @@ let unfold_all x gl = if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else tclIDTAC gl +(* Either unfold and clear if defined or simply clear if not a definition *) +let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id]) + (*****************************) (* High-level induction *) (*****************************) @@ -2829,7 +2832,9 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t let isrec, elim, indsign = get_eliminator elim gl in let names = compute_induction_names (Array.length indsign) names in (if isrec then tclTHENFIRSTn else tclTHENLASTn) - (tclTHEN (induct_tac elim) (tclTRY (thin indhyps))) + (tclTHEN + (induct_tac elim) + (tclMAP (fun id -> tclTRY (expand_hyp id)) (List.rev indhyps))) (array_map2 (induct_discharge destopt avoid tac) indsign names) gl (* Apply induction "in place" taking into account dependent |