Remplacement de Induction/Destruct par NewInduction/NewDestruct

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4463 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 13 deletions

diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 084538d8c..ee45a9476 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -26,35 +26,34 @@ Remark strip_commut:
       (commut A R1 R2)->(x,y:A)(clos_trans A R1 y x)->(z:A)(R2 z y)
             ->(EX y':A | (R2 y' x) & (clos_trans A R1 z y')).
 Proof.
- Induction 2;Intros.
- Elim H with y0 x0 z ;Auto with sets;Intros.
- Exists x1;Auto with sets.
+ NewInduction 2 as [x y|x y z H0 IH1 H1 IH2]; Intros.
+ Elim H with y x z ;Auto with sets;Intros x0 H2 H3.
+ Exists x0;Auto with sets.
 
- Elim H2 with z0 ;Auto with sets;Intros.
- Elim H4 with x1 ;Auto with sets;Intros.
- Exists x2;Auto with sets.
- Apply t_trans with x1 ;Auto with sets.
+ Elim IH1 with z0 ;Auto with sets;Intros.
+ Elim IH2 with x0 ;Auto with sets;Intros.
+ Exists x1;Auto with sets.
+ Apply t_trans with x0; Auto with sets.
 Qed.
 
 
   Lemma Acc_union:  (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x))
                          ->(a:A)(Acc A R2 a)->(Acc A Union a).
 Proof.
- Induction 3.
- Intros.
+ NewInduction 3 as [x H1 H2].
  Apply Acc_intro;Intros.
- Elim H4;Intros;Auto with sets.
+ Elim H3;Intros;Auto with sets.
  Cut (clos_trans A  R1 y x);Auto with sets.
  ElimType (Acc A (clos_trans A R1) y);Intros.
  Apply Acc_intro;Intros.
- Elim H9;Intros.
- Apply H7;Auto with sets.
+ Elim H8;Intros.
+ Apply H6;Auto with sets.
  Apply t_trans with x0 ;Auto with sets.
 
  Elim strip_commut with x x0 y0 ;Auto with sets;Intros.
  Apply Acc_inv_trans with x1 ;Auto with sets.
  Unfold union .
- Elim H12;Auto with sets;Intros.
+ Elim H11;Auto with sets;Intros.
  Apply t_trans with y1 ;Auto with sets.
 
  Apply (Acc_clos_trans A).