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

5 files changed, 37 insertions, 37 deletions

diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 9d24ae433..78ad3d2f2 100755
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -38,7 +38,7 @@ Qed.
 
 Lemma Noone_in_empty: (x: U) ~ (In U (Empty_set U) x).
 Proof.
-Intro x; Red; Induction 1.
+Red; NewDestruct 1.
 Qed.
 Hints Resolve Noone_in_empty.
 
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 1e0c05450..1e7168791 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -59,8 +59,8 @@ Lemma cardinal_invert :
    [n:nat] (EXT A | (EXT x | 
            X == (Add U A x) /\ ~ (In U A x) /\ (cardinal U A n))) end.
 Proof.
-Induction 1; Simpl; Auto.
-Intros; Exists A; Exists x; Auto.
+NewInduction 1; Simpl; Auto.
+Exists A; Exists x; Auto.
 Qed.
 
 Lemma cardinal_elim :
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index db41d6ac6..d5f42e3f9 100755
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -62,11 +62,11 @@ Split; Red; Intros x0 H'.
 Elim H'; Intros.
 Rewrite H0.
 Elim Add_inv with U X x x1; Auto with sets.
-Induction 1; Auto with sets.
+NewDestruct 1; Auto with sets.
 Elim Add_inv with V (Im X f) (f x) x0; Auto with sets.
-Induction 1; Intros.
-Rewrite H1; Auto with sets.
-Induction 1; Auto with sets.
+NewDestruct 1 as [x0 H y H0].
+Rewrite H0; Auto with sets.
+NewDestruct 1; Auto with sets.
 Qed.
 
 Lemma image_empty: (f: U -> V) (Im (Empty_set U) f) == (Empty_set V).
@@ -110,10 +110,10 @@ Unfold injective; Intros f H.
 Cut (EXT x | ~ ((y: U) (f x) == (f y) -> x == y)).
 2: Apply not_all_ex_not with P:=[x:U](y: U) (f x) == (f y) -> x == y; 
    Trivial with sets.
-Induction 1; Intros x C; Exists x.
+NewDestruct 1 as [x C]; Exists x.
 Cut (EXT y | ~((f x)==(f y)->x==y)).
 2: Apply not_all_ex_not with P:=[y:U](f x)==(f y)->x==y; Trivial with sets.
-Induction 1; Intros y D; Exists y.
+NewDestruct 1 as [y D]; Exists y.
 Apply imply_to_and; Trivial with sets.
 Qed.
 
@@ -140,21 +140,21 @@ Lemma injective_preserves_cardinal:
   (A: (Ensemble U)) (f: U -> V) (n: nat) (injective f) -> (cardinal ? A n) ->
    (n': nat) (cardinal ? (Im A f) n') -> n' = n.
 Proof.
-Induction 2; Auto with sets.
+NewInduction 2 as [|A n H'0 H'1 x H'2]; Auto with sets.
 Rewrite (image_empty f).
 Intros n' CE.
 Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intros A0 n0 H'0 H'1 x H'2 n'.
-Rewrite (Im_add A0 x f).
+Intro n'.
+Rewrite (Im_add A x f).
 Intro H'3.
-Elim cardinal_Im_intro with A0 f n0; Trivial with sets.
+Elim cardinal_Im_intro with A f n; Trivial with sets.
 Intros i CI.
 LApply (H'1 i); Trivial with sets.
-Cut ~ (In ? (Im A0 f) (f x)).
-Intros.
-Apply cardinal_unicity with V (Add ? (Im A0 f) (f x)); Trivial with sets.
+Cut ~ (In ? (Im A f) (f x)).
+Intros H0 H1.
+Apply cardinal_unicity with V (Add ? (Im A f) (f x)); Trivial with sets.
 Apply card_add; Auto with sets.
-Rewrite <- H2; Trivial with sets.
+Rewrite <- H1; Trivial with sets.
 Red; Intro; Apply H'2.
 Apply In_Image_elim with f; Trivial with sets.
 Qed.
@@ -163,17 +163,17 @@ Lemma cardinal_decreases:
   (A: (Ensemble U)) (f: U -> V) (n: nat) (cardinal U A n) ->
    (n': nat) (cardinal V (Im A f) n') -> (le n' n).
 Proof.
-Induction 1; Auto with sets.
+NewInduction 1 as [|A n H'0 H'1 x H'2]; Auto with sets.
 Rewrite (image_empty f); Intros.
 Cut n' = O.
 Intro E; Rewrite E; Trivial with sets.
 Apply cardinal_unicity with V (Empty_set V); Auto with sets.
-Intros A0 n0 H'0 H'1 x H'2 n'.
-Rewrite (Im_add A0 x f).
-Elim cardinal_Im_intro with A0 f n0; Trivial with sets.
+Intro n'.
+Rewrite (Im_add A x f).
+Elim cardinal_Im_intro with A f n; Trivial with sets.
 Intros p C H'3.
 Apply le_trans with (S p).
-Apply card_Add_gen with V (Im A0 f) (f x); Trivial with sets.
+Apply card_Add_gen with V (Im A f) (f x); Trivial with sets.
 Apply le_n_S; Auto with sets.
 Qed.
 
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 68d3ec7a5..37fb47e27 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -42,21 +42,21 @@ Hints Unfold  meq multiplicity.
 
 Lemma meq_refl : (x:multiset)(meq x x).
 Proof.
-Induction x; Auto.
+NewDestruct x; Auto.
 Qed.
 Hints Resolve meq_refl.
 
 Lemma meq_trans : (x,y,z:multiset)(meq x y)->(meq y z)->(meq x z).
 Proof.
 Unfold meq.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Rewrite H; Auto.
 Qed.
 
 Lemma meq_sym : (x,y:multiset)(meq x y)->(meq y x).
 Proof.
 Unfold meq.
-Induction x; Induction y; Auto.
+NewDestruct x; NewDestruct y; Auto.
 Qed.
 Hints Immediate meq_sym.
 
@@ -83,7 +83,7 @@ Require Plus. (* comm. and ass. of plus *)
 Lemma munion_comm : (x,y:multiset)(meq (munion x y) (munion y x)).
 Proof.
 Unfold meq; Unfold multiplicity; Unfold munion.
-Induction x; Induction y; Auto with arith.
+NewDestruct x; NewDestruct y; Auto with arith.
 Qed.
 Hints Resolve munion_comm.
 
@@ -91,14 +91,14 @@ Lemma munion_ass :
       (x,y,z:multiset)(meq (munion (munion x y) z) (munion x (munion y z))).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z; Auto with arith.
+NewDestruct x; NewDestruct y; NewDestruct z; Auto with arith.
 Qed.
 Hints Resolve munion_ass.
 
 Lemma meq_left :  (x,y,z:multiset)(meq x y)->(meq (munion x z) (munion y z)).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto with arith.
 Qed.
 Hints Resolve meq_left.
@@ -106,7 +106,7 @@ Hints Resolve meq_left.
 Lemma meq_right : (x,y,z:multiset)(meq x y)->(meq (munion z x) (munion z y)).
 Proof.
 Unfold meq; Unfold munion; Unfold multiplicity.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve meq_right.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 17b10ae3a..5b28d6c2b 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -54,7 +54,7 @@ Hints Unfold seq.
 
 Lemma leb_refl : (b:bool)(leb b b).
 Proof.
-Induction b; Simpl; Auto.
+NewDestruct b; Simpl; Auto.
 Qed.
 Hints Resolve leb_refl.
 
@@ -70,21 +70,21 @@ Qed.
 
 Lemma seq_refl : (x:uniset)(seq x x).
 Proof.
-Induction x; Unfold seq; Auto.
+NewDestruct x; Unfold seq; Auto.
 Qed.
 Hints Resolve seq_refl.
 
 Lemma seq_trans : (x,y,z:uniset)(seq x y)->(seq y z)->(seq x z).
 Proof.
 Unfold seq.
-Induction x; Induction y; Induction z; Simpl; Intros.
+NewDestruct x; NewDestruct y; NewDestruct z; Simpl; Intros.
 Rewrite H; Auto.
 Qed.
 
 Lemma seq_sym : (x,y:uniset)(seq x y)->(seq y x).
 Proof.
 Unfold seq.
-Induction x; Induction y; Simpl; Auto.
+NewDestruct x; NewDestruct y; Simpl; Auto.
 Qed.
 
 (** uniset union *)
@@ -109,7 +109,7 @@ Hints Resolve union_empty_right.
 Lemma union_comm : (x,y:uniset)(seq (union x y) (union y x)).
 Proof.
 Unfold seq; Unfold charac; Unfold union.
-Induction x; Induction y; Auto with bool.
+NewDestruct x; NewDestruct y; Auto with bool.
 Qed.
 Hints Resolve union_comm.
 
@@ -117,14 +117,14 @@ Lemma union_ass :
       (x,y,z:uniset)(seq (union (union x y) z) (union x (union y z))).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z; Auto with bool.
+NewDestruct x; NewDestruct y; NewDestruct z; Auto with bool.
 Qed.
 Hints Resolve union_ass.
 
 Lemma seq_left :  (x,y,z:uniset)(seq x y)->(seq (union x z) (union y z)).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve seq_left.
@@ -132,7 +132,7 @@ Hints Resolve seq_left.
 Lemma seq_right : (x,y,z:uniset)(seq x y)->(seq (union z x) (union z y)).
 Proof.
 Unfold seq; Unfold union; Unfold charac.
-Induction x; Induction y; Induction z.
+NewDestruct x; NewDestruct y; NewDestruct z.
 Intros; Elim H; Auto.
 Qed.
 Hints Resolve seq_right.