4 files changed, 16 insertions, 16 deletions
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 27c760194..65571855e 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -35,11 +35,11 @@ Require Zsyntax.
 
 Lemma inject_nat_complete :
   (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
-Destruct x; Intros;
+NewDestruct x; Intros;
 [ Exists  O; Auto with arith
 | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
-  Exists (S x0); Intros; Simpl;
-  Specialize (bij1 x0); Intro Hx0;
+  Exists (S x); Intros; Simpl;
+  Specialize (bij1 x); Intro Hx0;
   Rewrite <- H0 in Hx0;
   Apply f_equal with f:=POS;
   Apply convert_intro; Auto with arith
@@ -61,7 +61,7 @@ Save.
 
 Lemma inject_nat_complete_inf :
   (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }.
-Destruct x; Intros;
+NewDestruct x; Intros;
 [ Exists  O; Auto with arith
 | Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0;
   Exists (S x0); Intros; Simpl;
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index dc9e69e17..cf46b8bdf 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -261,12 +261,12 @@ Save.
 
 Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
 Proof.
-  Destruct z; [ Idtac | Destruct p | Destruct p  ]; Compute; Trivial.
+  NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
 Save.
 
 Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z).
 Proof.
-  Destruct z; [ Idtac | Destruct p | Destruct p  ]; Compute; Trivial.
+  NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
 Save.
 
 Hints Unfold Zeven Zodd : zarith.
@@ -291,22 +291,22 @@ Definition Zdiv2 :=
 
 Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`.
 Proof.
-Destruct x.
+NewDestruct x.
 Auto with arith.
-Destruct p; Auto with arith.
-Intros. Absurd (Zeven (POS (xI p0))); Red; Auto with arith.
+NewDestruct p; Auto with arith.
+Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith.
 Intros. Absurd (Zeven `1`); Red; Auto with arith.
-Destruct p; Auto with arith.
-Intros. Absurd (Zeven (NEG (xI p0))); Red; Auto with arith.
+NewDestruct p; Auto with arith.
+Intros. Absurd (Zeven (NEG (xI p))); Red; Auto with arith.
 Intros. Absurd (Zeven `-1`); Red; Auto with arith.
 Save.
 
 Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`.
 Proof.
-Destruct x.
+NewDestruct x.
 Intros. Absurd (Zodd `0`); Red; Auto with arith.
-Destruct p; Auto with arith.
-Intros. Absurd (Zodd (POS (xO p0))); Red; Auto with arith.
+NewDestruct p; Auto with arith.
+Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith.
 Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith.
 Save.
 
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index f64093034..678e8b472 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1147,7 +1147,7 @@ Save.
 Theorem Zmult_Zopp_Zopp:
   (x,y:Z) (Zmult (Zopp x) (Zopp y)) = (Zmult x y).
 Proof.
-Destruct x; Destruct y; Reflexivity.
+NewDestruct x; NewDestruct y; Reflexivity.
 Save.
 
 Theorem weak_Zmult_plus_distr_r:
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 72b66c494..7eb1e37c2 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -46,7 +46,7 @@ Definition Zabs [z:Z] : Z :=
 (*s Properties of absolu function *)
 
 Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
-Destruct x; Auto with arith.
+NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Save.