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

3 files changed, 10 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 775a2220ce..b97fdfe058 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.