Expérimentation de NewDestruct et parfois NewInduction

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

8 files changed, 36 insertions, 36 deletions

diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index 52607a4a0d..90d1f59408 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -18,7 +18,7 @@ Require Wf_nat.
 Implicit Arguments On.
 
 Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`.
-Destruct x; Destruct y; Auto.
+NewDestruct x; NewDestruct y; Auto.
 Simpl; Intros; Discriminate H.
 Simpl; Intros; Discriminate H.
 Simpl; Intros; Discriminate H.
@@ -153,23 +153,23 @@ Save.
 Section diveucl.
 
 Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. 
-Destruct x.
+NewDestruct x.
 Left ; Split with ZERO; Reflexivity.
 
-Destruct p.
-Right ; Split with (POS p0); Reflexivity.
+NewDestruct p.
+Right ; Split with (POS p); Reflexivity.
 
-Left ; Split with (POS p0); Reflexivity.
+Left ; Split with (POS p); Reflexivity.
 
 Right ; Split with ZERO; Reflexivity.
 
-Destruct p.
-Right ; Split with (NEG (add xH p0)).
+NewDestruct p.
+Right ; Split with (NEG (add xH p)).
 Rewrite NEG_xI.
 Rewrite NEG_add.
 Omega.
 
-Left ; Split with (NEG p0); Reflexivity.
+Left ; Split with (NEG p); Reflexivity.
 
 Right ; Split with `-1`; Reflexivity.
 Save.
@@ -273,7 +273,7 @@ Save.
 
 Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z)
   { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }.
-Destruct a;
+NewDestruct a;
 
 [ (* a=0 *) Exists `(0,0)`; Omega
 | (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index c2585b3e08..1d97275736 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -78,7 +78,7 @@ Hints Unfold  Zpower_nat : zarith.
 
 Lemma Zpower_exp : (x:Z)(n,m:Z)
   `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
-Destruct n; Destruct m; Auto with zarith.
+NewDestruct n; NewDestruct m; Auto with zarith.
 Simpl; Intros; Apply Zred_factor0.
 Simpl; Auto with zarith.
 Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
@@ -313,7 +313,7 @@ Elim (convert p); Simpl;
 | Intro n; Rewrite (two_power_nat_S n);
   Unfold 2 Zdiv_rest_aux;
   Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`));
-  Destruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
+  NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
 Save.
 
 Lemma Zdiv_rest_correct2 :
@@ -330,33 +330,33 @@ Intros; Apply iter_pos_invariant with
   Intros q r d; Unfold Zdiv_rest_aux; 
   Elim q;
   [ Omega
-  | Destruct p0; 
-    [ Intro; Rewrite POS_xI; Intro; Elim H; Intros; Split; 
+  | NewDestruct p0; 
+    [ Rewrite POS_xI; Intro; Elim H; Intros; Split; 
       [ Rewrite H0; Rewrite Zplus_assoc;
       	Rewrite Zmult_plus_distr_l;
       	Rewrite Zmult_1_n; Rewrite Zmult_assoc;
-      	Rewrite (Zmult_sym (POS p1) `2`); Apply refl_equal
+      	Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal
       | Omega ]
-    | Intro; Rewrite POS_xO; Intro; Elim H; Intros; Split;
+    | Rewrite POS_xO; Intro; Elim H; Intros; Split;
       [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p1) `2`);
+      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`);
       	Apply refl_equal  
       | Omega ]
     | Omega ]
-  | Destruct p0; 
-    [ Intro; Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
+  | NewDestruct p0; 
+    [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
       [ Rewrite H0; Rewrite Zplus_assoc;
       	Apply f_equal with f:=[z:Z]`z+r`;
       	Do 2 (Rewrite Zmult_plus_distr_l);
        	Rewrite Zmult_assoc; 
-      	Rewrite (Zmult_sym (NEG p1) `2`);
+      	Rewrite (Zmult_sym (NEG p0) `2`);
       	Rewrite <- Zplus_assoc;
-	Apply f_equal with f:=[z:Z]`2 * (NEG p1) * d + z`; 
+	Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; 
       	Omega
       | Omega ]
-    | Intro; Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split;
+    | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split;
       [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p1) `2`);
+      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`);
       	Apply refl_equal  
       | Omega ]
     | Omega ] ]
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 88e609e3f8..93c6eaf539 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -69,15 +69,15 @@ Grammar vernac vernac : ast :=
 
 Definition BoolTheory : (Ring_Theory xorb andb true false [b:bool]b eqb).
 Split; Simpl.
-Destruct n; Destruct m; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct n; Destruct m; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Reflexivity.
-Destruct n; Destruct m; Destruct p; Reflexivity.
-Destruct x; Destruct y; Reflexivity Orelse Simpl; Tauto.
+NewDestruct n; NewDestruct m; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct n; NewDestruct m; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; Reflexivity.
+NewDestruct n; NewDestruct m; NewDestruct p; Reflexivity.
+NewDestruct x; NewDestruct y; Reflexivity Orelse Simpl; Tauto.
 Defined.
 
 Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ].
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 05a6f68507..80d27e630d 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -208,7 +208,7 @@ Proof.
   Induction x.
   Intros; Simpl; EAuto.
 
-  Destruct y; Intros.
+  NewDestruct y; Intros.
 
   Simpl; Rewrite H; EAuto.
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index f44f554e0e..ae72f4eb4c 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -427,7 +427,7 @@ Save.
 Remark interp_m_ok : (x:A)(l:varlist)
   (interp_m x l)==(Amult x (interp_vl l)).
 Proof.
-  Destruct l.
+  NewDestruct l.
   Simpl; Trivial.
   Reflexivity.
 Save.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 8b4a0f95d3..1b787f4239 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -386,7 +386,7 @@ Definition Semi_Ring_Theory_of :
   (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool)
   (Ring_Theory Aplus Amult Aone Azero Aopp Aeq)
     ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq).
-Destruct 1.
+Intros until 1; Case H.
 Split; Intros; Simpl; EAuto.
 Defined.
 
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 9b74e8952c..04e2aa16ab 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -453,7 +453,7 @@ Save.
 Remark interp_m_ok : (x:A)(l:varlist)
   (Aequiv (interp_m x l) (Amult x (interp_vl l))).
 Proof.
-  Destruct l;Trivial.
+  NewDestruct l;Trivial.
 Save.
 
 Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 6428947ec0..a0d587eb34 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -434,7 +434,7 @@ Implicit Arguments Off.
 
 Definition Semi_Setoid_Ring_Theory_of :
   Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
-Destruct 1.
+NewDestruct 1.
 Split; Intros; Simpl; EAuto.
 Defined.