diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 4 |
3 files changed, 10 insertions, 3 deletions
@@ -28,6 +28,8 @@ Tactics - New experimental tactical "timeout <n> <tac>". Since <n> is a time in second for the moment, this feature should rather be avoided in scripts meant to be machine-independent. +- Fixing a bug of destruct that left local definitions in context might result in + some rare incompatibilities (solvable by adapting name hypotheses). Vernacular commands 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 diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 4570fde726..ec18d8dc57 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -626,12 +626,12 @@ Proof. induction q as [ | p q IHq ]. apply eq_dep_eq_positive. cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial. - destruct p0; intros; discriminate. + destruct p; intros; discriminate. trivial. apply eq_dep_eq_positive. cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. intro. destruct p; discriminate. - intro. unfold p0 in H. apply Psucc_inj in H. + intro. apply Psucc_inj in H. generalize q'. rewrite H. intro. rewrite (IHq q'0). trivial. |