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

29 files changed, 197 insertions, 197 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index ab22eca22..e6b444601 100755
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -22,29 +22,29 @@ Hint constr_between : arith v62 := Constructors between.
 
 Lemma bet_eq : (k,l:nat)(l=k)->(between k l).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Hints Resolve bet_eq : arith v62.
 
 Lemma between_le : (k,l:nat)(between k l)->(le k l).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 Hints Immediate between_le : arith v62.
 
 Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l).
 Proof.
-Induction 1.
+NewInduction 1.
 Intros; Absurd (le (S k) k); Auto with arith.
-Induction 1; Auto with arith.
+Induction H; Auto with arith.
 Qed.
 Hints Resolve between_Sk_l : arith v62.
 
 Lemma between_restr : 
   (k,l,m:nat)(le k l)->(le l m)->(between k m)->(between l m).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Inductive exists [k:nat] : nat -> Prop
@@ -55,7 +55,7 @@ Hint constr_exists : arith v62 := Constructors exists.
 
 Lemma exists_le_S : (k,l:nat)(exists k l)->(le (S k) l).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Lemma exists_lt : (k,l:nat)(exists k l)->(lt k l).
@@ -78,55 +78,55 @@ Hints Resolve in_int_intro : arith v62.
 
 Lemma in_int_lt : (p,q,r:nat)(in_int p q r)->(lt p q).
 Proof.
-Induction 1; Intros.
+NewInduction 1; Intros.
 Apply le_lt_trans with r; Auto with arith.
 Qed.
 
 Lemma in_int_p_Sq : 
   (p,q,r:nat)(in_int p (S q) r)->((in_int p q r) \/ <nat>r=q).
 Proof.
-Induction 1; Intros.
+NewInduction 1; Intros.
 Elim (le_lt_or_eq r q); Auto with arith.
 Qed.
 
 Lemma in_int_S : (p,q,r:nat)(in_int p q r)->(in_int p (S q) r).
 Proof.
-Induction 1;Auto with arith.
+NewInduction 1;Auto with arith.
 Qed.
 Hints Resolve in_int_S : arith v62.
 
 Lemma in_int_Sp_q : (p,q,r:nat)(in_int (S p) q r)->(in_int p q r).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 Hints Immediate in_int_Sp_q : arith v62.
 
 Lemma between_in_int : (k,l:nat)(between k l)->(r:nat)(in_int k l r)->(P r).
 Proof.
-Induction 1; Intros.
+NewInduction 1; Intros.
 Absurd (lt k k); Auto with arith.
 Apply in_int_lt with r; Auto with arith.
-Elim (in_int_p_Sq k l0 r); Intros; Auto with arith.
-Rewrite H4; Trivial with arith.
+Elim (in_int_p_Sq k l r); Intros; Auto with arith.
+Rewrite H2; Trivial with arith.
 Qed.
 
 Lemma in_int_between : 
   (k,l:nat)(le k l)->((r:nat)(in_int k l r)->(P r))->(between k l).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Lemma exists_in_int : 
   (k,l:nat)(exists k l)->(EX m:nat | (in_int k l m) & (Q m)).
 Proof.
-Induction 1.
-Induction 2; Intros p inp Qp; Exists p; Auto with arith.
-Intros; Exists l0; Auto with arith.
+NewInduction 1.
+Case IHexists; Intros p inp Qp; Exists p; Auto with arith.
+Exists l; Auto with arith.
 Qed.
 
 Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l).
 Proof.
-Induction 1; Intros.
+NewInduction 1; Intros.
 Elim H1; Auto with arith.
 Qed.
 
@@ -134,23 +134,23 @@ Lemma between_or_exists :
   (k,l:nat)(le k l)->((n:nat)(in_int k l n)->((P n)\/(Q n)))
      ->((between k l)\/(exists k l)).
 Proof.
-Induction 1; Intros; Auto with arith.
-Elim H1; Intro; Auto with arith.
-Elim (H2 m); Auto with arith.
+NewInduction 1; Intros; Auto with arith.
+Elim IHle; Intro; Auto with arith.
+Elim (H0 m); Auto with arith.
 Qed.
 
 Lemma between_not_exists : (k,l:nat)(between k l)->
      ((n:nat)(in_int k l n) -> (P n) -> ~(Q n))
      -> ~(exists k l).
 Proof.
-Induction 1; Red; Intros.
+NewInduction 1; Red; Intros.
 Absurd (lt k k); Auto with arith.
-Absurd (Q l0); Auto with arith.
-Elim (exists_in_int k (S l0)); Auto with arith; Intros l' inl' Ql'.
-Replace l0 with l'; Auto with arith.
+Absurd (Q l); Auto with arith.
+Elim (exists_in_int k (S l)); Auto with arith; Intros l' inl' Ql'.
+Replace l with l'; Auto with arith.
 Elim inl'; Intros.
-Elim (le_lt_or_eq l' l0); Auto with arith; Intros.
-Absurd (exists k l0); Auto with arith.
+Elim (le_lt_or_eq l' l); Auto with arith; Intros.
+Absurd (exists k l); Auto with arith.
 Apply in_int_exists with l'; Auto with arith.
 Qed.
 
@@ -161,7 +161,7 @@ Inductive nth [init:nat] : nat->nat->Prop
 
 Lemma nth_le : (init,l,n:nat)(nth init l n)->(le init l).
 Proof.
-Induction 1; Intros; Auto with arith.
+NewInduction 1; Intros; Auto with arith.
 Apply le_trans with (S k); Auto with arith.
 Qed.
 
@@ -169,7 +169,7 @@ Definition eventually := [n:nat](EX k:nat | (le k n) & (Q k)).
 
 Lemma event_O : (eventually O)->(Q O).
 Proof.
-Induction 1; Intros.
+NewInduction 1; Intros.
 Replace O with x; Auto with arith.
 Qed.
 
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 172ccf568..cc4399d2f 100755
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -43,7 +43,7 @@ Proof.
 Intros m n H.
 LApply (lt_le_S m n); Auto with arith.
 Intro H'; LApply (le_lt_or_eq (S m) n); Auto with arith.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Right; Exists (minus n (S (S m))); Simpl.
 Rewrite (plus_sym m (minus n (S (S m)))).
 Rewrite (plus_n_Sm (minus n (S (S m))) m).
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 1397326b2..531e0a975 100755
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -14,14 +14,14 @@ Require Gt.
 Require Decidable.
 
 Theorem zerop : (n:nat){n=O}+{lt O n}.
-Destruct n; Auto with arith.
+NewDestruct n; Auto with arith.
 Save.
 
 Theorem lt_eq_lt_dec : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}.
 Proof.
-Induction n; Induction m; Auto with arith.
-Intros q H'; Elim (H q).
-Induction 1; Auto with arith.
+NewInduction n; NewInduction m; Auto with arith.
+Elim (IHn m).
+NewInduction 1; Auto with arith.
 Auto with arith.
 Qed.
 
@@ -30,11 +30,11 @@ Proof lt_eq_lt_dec.
 
 Lemma le_lt_dec : (n,m:nat) {le n m} + {lt m n}.
 Proof.
-Induction n.
+NewInduction n.
 Auto with arith.
-Induction m.
+NewInduction m.
 Auto with arith.
-Intros q H'; Elim (H q); Auto with arith.
+Elim (IHn m); Auto with arith.
 Qed.
 
 Lemma le_le_S_dec : (n,m:nat) {le n m} + {le (S m) n}.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 60fdc68ff..2a087a06d 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -32,8 +32,8 @@ Intros.
 Cut (n:nat)(P n)/\(P (S n)).
 Intros. Elim (H2 n). Auto with arith.
 
-Induction n0. Auto with arith.
-Intros. Elim H2; Auto with arith.
+NewInduction n0. Auto with arith.
+Intros. Elim IHn0; Auto with arith.
 Qed.
 
 (* 0 <n  =>  n/2 < n *)
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 8392f17ce..d0bd9afc6 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -21,17 +21,17 @@ Fixpoint  eq_nat [n:nat] : nat -> Prop :=
           end.
 
 Theorem eq_nat_refl : (n:nat)(eq_nat n n).
-Induction n; Simpl; Auto.
+NewInduction n; Simpl; Auto.
 Qed.
 Hints Resolve eq_nat_refl : arith v62.
 
 Theorem eq_eq_nat : (n,m:nat)(n=m)->(eq_nat n m).
-Induction 1; Trivial with arith.
+NewInduction 1; Trivial with arith.
 Qed.
 Hints Immediate eq_eq_nat : arith v62.
 
 Theorem eq_nat_eq : (n,m:nat)(eq_nat n m)->(n=m).
-Induction n; Induction m; Simpl; Contradiction Orelse Auto with arith.
+NewInduction n; NewInduction m; Simpl; Contradiction Orelse Auto with arith.
 Qed.
 Hints Immediate eq_nat_eq : arith v62.
 
@@ -40,15 +40,15 @@ Intros; Replace m with n; Auto with arith.
 Qed.
 
 Theorem eq_nat_decide : (n,m:nat){(eq_nat n m)}+{~(eq_nat n m)}.
-Induction n.
-Destruct m.
+NewInduction n.
+NewDestruct m.
 Auto with arith.
-Intro; Right; Red; Trivial with arith.
-Destruct m.
+Intros; Right; Red; Trivial with arith.
+NewDestruct m.
 Right; Red; Auto with arith.
 Intros.
 Simpl.
-Apply H.
+Apply IHn.
 Defined.
 
 Fixpoint  beq_nat [n:nat] : nat -> bool :=
@@ -61,7 +61,7 @@ Fixpoint  beq_nat [n:nat] : nat -> bool :=
 
 Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
 Proof.
-  Induction x; Simpl; Auto.
+  NewInduction x; Simpl; Auto.
 Qed.
 
 Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index bf73ecb0a..0f1ab8559 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -24,22 +24,22 @@ Hint constr_odd : arith := Constructors odd.
 
 Lemma even_or_odd : (n:nat) (even n)\/(odd n).
 Proof.
-Induction n.
+NewInduction n.
 Auto with arith.
-Intros n' H. Elim H; Auto with arith.
+Elim IHn; Auto with arith.
 Save.
 
 Lemma even_odd_dec : (n:nat) { (even n) }+{ (odd n) }.
 Proof.
-Induction n.
+NewInduction n.
 Auto with arith.
-Intros n' H. Elim H; Auto with arith.
+Elim IHn; Auto with arith.
 Save.
 
 Lemma not_even_and_odd : (n:nat) (even n) -> (odd n) -> False.
 Proof.
-Induction n.
+NewInduction n.
 Intros. Inversion H0.
-Intros. Inversion H0. Inversion H1. Auto with arith.
+Intros. Inversion H. Inversion H0. Auto with arith.
 Save.
 
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index be420c672..db4494fdf 100755
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -14,12 +14,12 @@
 
 Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)).
 Proof.
-  Induction 1; Auto.
+  NewInduction 1; Auto.
 Qed.
 
 Theorem le_trans : (n,m,p:nat)(le n m)->(le m p)->(le n p).
 Proof.
-  Induction 2; Auto.
+  NewInduction 2; Auto.
 Qed.
 
 Theorem le_n_Sn : (n:nat)(le n (S n)).
@@ -29,14 +29,14 @@ Qed.
 
 Theorem le_O_n : (n:nat)(le O n).
 Proof.
-  Induction n ; Auto.
+  NewInduction n ; Auto.
 Qed.
 
 Hints Resolve le_n_S le_n_Sn le_O_n le_n_S le_trans : arith v62.
 
 Theorem le_pred_n : (n:nat)(le (pred n) n).
 Proof.
-Induction n ; Auto with arith.
+NewInduction n ; Auto with arith.
 Qed.
 Hints Resolve le_pred_n : arith v62.
 
@@ -73,7 +73,7 @@ Hints Resolve le_Sn_O : arith v62.
 
 Theorem le_Sn_n : (n:nat)~(le (S n) n).
 Proof.
-Induction n; Auto with arith.
+NewInduction n; Auto with arith.
 Qed.
 Hints Resolve le_Sn_n : arith v62.
 
@@ -110,7 +110,7 @@ Lemma le_elim_rel : (P:nat->nat->Prop)
      ((p,q:nat)(le p q)->(P p q)->(P (S p) (S q)))->
      (n,m:nat)(le n m)->(P n m).
 Proof.
-Induction n; Auto with arith.
-Intros n' HRec m Le.
+NewInduction n; Auto with arith.
+Intros m Le.
 Elim Le; Auto with arith.
 Qed.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 785685093..7b5e089c3 100755
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -50,17 +50,17 @@ Hints Resolve lt_n_n : arith v62.
 
 Lemma S_pred : (n,m:nat)(lt m n)->(n=(S (pred n))).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Lemma lt_pred : (n,p:nat)(lt (S n) p)->(lt n (pred p)).
 Proof.
-Induction 1; Simpl; Auto with arith.
+NewInduction 1; Simpl; Auto with arith.
 Qed.
 Hints Immediate lt_pred : arith v62.
 
 Lemma lt_pred_n_n : (n:nat)(lt O n)->(lt (pred n) n).
-Destruct 1; Simpl; Auto with arith.
+NewDestruct 1; Simpl; Auto with arith.
 Save.
 Hints Resolve lt_pred_n_n : arith v62.
 
@@ -92,14 +92,14 @@ Hints Immediate lt_le_weak : arith v62.
 
 Theorem neq_O_lt : (n:nat)(~O=n)->(lt O n).
 Proof.
-Induction n; Auto with arith.
+NewInduction n; Auto with arith.
 Intros; Absurd O=O; Trivial with arith.
 Qed.
 Hints Immediate neq_O_lt : arith v62.
 
 Theorem lt_O_neq : (n:nat)(lt O n)->(~O=n).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 Hints Immediate lt_O_neq : arith v62.
 
@@ -107,35 +107,35 @@ Hints Immediate lt_O_neq : arith v62.
 
 Theorem lt_trans : (n,m,p:nat)(lt n m)->(lt m p)->(lt n p).
 Proof.
-Induction 2; Auto with arith.
+NewInduction 2; Auto with arith.
 Qed.
 
 Theorem lt_le_trans : (n,m,p:nat)(lt n m)->(le m p)->(lt n p).
 Proof.
-Induction 2; Auto with arith.
+NewInduction 2; Auto with arith.
 Qed.
 
 Theorem le_lt_trans : (n,m,p:nat)(le n m)->(lt m p)->(lt n p).
 Proof.
-Induction 2; Auto with arith.
+NewInduction 2; Auto with arith.
 Qed.
 
 Hints Resolve lt_trans lt_le_trans le_lt_trans : arith v62.
 
 Theorem le_lt_or_eq : (n,m:nat)(le n m)->((lt n m) \/ n=m).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Theorem le_or_lt : (n,m:nat)((le n m)\/(lt m n)).
 Proof.
 Intros n m; Pattern n m; Apply nat_double_ind; Auto with arith.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Theorem le_not_lt : (n,m:nat)(le n m) -> ~(lt m n).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Theorem lt_not_le : (n,m:nat)(lt n m) -> ~(le m n).
@@ -146,7 +146,7 @@ Hints Immediate le_not_lt lt_not_le : arith v62.
 
 Theorem lt_not_sym : (n,m:nat)(lt n m) -> ~(lt m n).
 Proof.
-Induction 1; Auto with arith.
+NewInduction 1; Auto with arith.
 Qed.
 
 Theorem nat_total_order: (m,n: nat) ~ m = n -> (lt m n) \/ (lt n m).
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index bc976fbd2..a38329c34 100755
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -28,15 +28,15 @@ Qed.
 
 Lemma le_min_l : (n,m:nat)(le (min n m) n).
 Proof.
-Induction n; Intros; Simpl; Auto with arith.
+NewInduction n; Intros; Simpl; Auto with arith.
 Elim m; Intros; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_min_l : arith v62.
 
 Lemma le_min_r : (n,m:nat)(le (min n m) m).
 Proof.
-Induction n; Simpl; Auto with arith.
-Induction m; Simpl; Auto with arith.
+NewInduction n; Simpl; Auto with arith.
+NewInduction m; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_min_r : arith v62.
 
@@ -44,7 +44,7 @@ Hints Resolve le_min_r : arith v62.
 
 Lemma min_case : (n,m:nat)(P:nat->Set)(P n)->(P m)->(P (min n m)).
 Proof.
-Induction n; Simpl; Auto with arith.
-Induction m; Intros; Simpl; Auto with arith.
-Pattern (min n0 n1); Apply H ; Auto with arith.
+NewInduction n; Simpl; Auto with arith.
+NewInduction m; Intros; Simpl; Auto with arith.
+Pattern (min n m); Apply IHn ; Auto with arith.
 Qed.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 3da5916e0..f3f67dea3 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -27,19 +27,19 @@ Fixpoint minus [n:nat] : nat -> nat :=
 Lemma minus_plus_simpl : 
 	(n,m,p:nat)((minus n m)=(minus (plus p n) (plus p m))).
 Proof.
-  Induction p; Simpl; Auto with arith.
+  NewInduction p; Simpl; Auto with arith.
 Qed.
 Hints Resolve minus_plus_simpl : arith v62.
 
 Lemma minus_n_O : (n:nat)(n=(minus n O)).
 Proof.
-Induction n; Simpl; Auto with arith.
+NewInduction n; Simpl; Auto with arith.
 Qed.
 Hints Resolve minus_n_O : arith v62.
 
 Lemma minus_n_n : (n:nat)(O=(minus n n)).
 Proof.
-Induction n; Simpl; Auto with arith.
+NewInduction n; Simpl; Auto with arith.
 Qed.
 Hints Resolve minus_n_n : arith v62.
 
@@ -84,7 +84,7 @@ Intros; Absurd (lt O O); Auto with arith.
 Intros p q lepq Hp gtp.
 Elim (le_lt_or_eq O p); Auto with arith.
 Auto with arith.
-Induction 1; Elim minus_n_O; Auto with arith.
+NewInduction 1; Elim minus_n_O; Auto with arith.
 Qed.
 Hints Resolve lt_minus : arith v62.
 
@@ -96,7 +96,7 @@ Qed.
 Hints Immediate lt_O_minus_lt : arith v62.
 
 Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
-Induction x; Auto with arith.
+NewInduction x; Auto with arith.
 Save.
 
 
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 8955b1ea3..86404aca3 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -26,8 +26,8 @@ Hints Resolve mult_plus_distr : arith v62.
 
 Lemma mult_plus_distr_r : (n,m,p:nat) (mult n (plus m p))=(plus (mult n m) (mult n p)).
 Proof.
-  Induction n. Trivial.
-  Intros. Simpl. Rewrite (H m p). Apply sym_eq. Apply plus_permute_2_in_4.
+  NewInduction n. Trivial.
+  Intros. Simpl. Rewrite (IHn m p). Apply sym_eq. Apply plus_permute_2_in_4.
 Qed.
 
 Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
@@ -39,7 +39,7 @@ Hints Resolve mult_minus_distr : arith v62.
 
 Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).
 Proof.
-Induction m; Simpl; Auto with arith.
+NewInduction m; Simpl; Auto with arith.
 Qed.
 Hints Resolve mult_O_le : arith v62.
 
@@ -76,16 +76,16 @@ Hints Resolve mult_n_1 : arith v62.
 
 Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
 Proof.
-  Induction m. Intros. Simpl. Apply le_n.
+  NewInduction m. Intros. Simpl. Apply le_n.
   Intros. Simpl. Apply le_plus_plus. Assumption.
-  Apply H. Assumption.
+  Apply IHm. Assumption.
 Qed.
 Hints Resolve mult_le : arith.
 
 Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
 Proof.
-  Induction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
-  Intros. Exact (lt_plus_plus ? ? ? ? H0 (H ? ? H0)).
+  NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
+  Intros. Exact (lt_plus_plus ? ? ? ? H (IHm ? ? H)).
 Qed.
 
 Hints Resolve mult_lt : arith.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index b02d5a324..d847a060d 100755
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -12,20 +12,20 @@ Require Decidable.
 
 Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}.
 Proof.
-Induction n.
+NewInduction n.
 Auto.
-Intros p H; Left; Exists p; Auto.
+Left; Exists n; Auto.
 Qed.
 
 Theorem eq_nat_dec : (n,m:nat){n=m}+{~(n=m)}.
 Proof.
-Induction n; Induction m; Auto.
-Intros q H'; Elim (H q); Auto.
+NewInduction n; NewInduction m; Auto.
+Elim (IHn m); Auto.
 Qed.
 
 Hints Resolve O_or_S eq_nat_dec : arith.
 
 Theorem dec_eq_nat:(x,y:nat)(decidable (x=y)).
 Intros x y; Unfold decidable; Elim (eq_nat_dec x y); Auto with arith.
-Save.
+Qed.
 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 1b70e1512..69bbd975a 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -32,7 +32,7 @@ Qed.
 
 Lemma simpl_plus_l : (n,m,p:nat)((plus n m)=(plus n p))->(m=p).
 Proof.
-Induction n ; Simpl ; Auto with arith.
+NewInduction n ; Simpl ; Auto with arith.
 Qed.
 
 Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)).
@@ -54,18 +54,18 @@ Hints Resolve plus_assoc_r : arith v62.
 
 Lemma simpl_le_plus_l : (p,n,m:nat)(le (plus p n) (plus p m))->(le n m).
 Proof.
-Induction p; Simpl; Auto with arith.
+NewInduction p; Simpl; Auto with arith.
 Qed.
 
 Lemma le_reg_l : (n,m,p:nat)(le n m)->(le (plus p n) (plus p m)).
 Proof.
-Induction p; Simpl; Auto with arith.
+NewInduction p; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_reg_l : arith v62.
 
 Lemma le_reg_r : (a,b,c:nat) (le a b)->(le (plus a c) (plus b c)).
 Proof.
-Induction 1 ; Simpl; Auto with arith.
+NewInduction 1 ; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_reg_r : arith v62.
 
@@ -78,7 +78,7 @@ Qed.
 
 Lemma le_plus_l : (n,m:nat)(le n (plus n m)).
 Proof.
-Induction n; Simpl; Auto with arith.
+NewInduction n; Simpl; Auto with arith.
 Qed.
 Hints Resolve le_plus_l : arith v62.
 
@@ -96,12 +96,12 @@ Hints Resolve le_plus_trans : arith v62.
 
 Lemma simpl_lt_plus_l : (n,m,p:nat)(lt (plus p n) (plus p m))->(lt n m).
 Proof.
-Induction p; Simpl; Auto with arith.
+NewInduction p; Simpl; Auto with arith.
 Qed.
 
 Lemma lt_reg_l : (n,m,p:nat)(lt n m)->(lt (plus p n) (plus p m)).
 Proof.
-Induction p; Simpl; Auto with arith.
+NewInduction p; Simpl; Auto with arith.
 Qed.
 Hints Resolve lt_reg_l : arith v62.
 
@@ -138,15 +138,15 @@ Qed.
 
 Lemma plus_is_O : (m,n:nat) (plus m n)=O -> m=O /\ n=O.
 Proof.
-  Destruct m; Auto.
+  NewDestruct m; Auto.
   Intros. Discriminate H.
 Qed.
 
 Lemma plus_is_one : 
       (m,n:nat) (plus m n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
-  Destruct m; Auto.
-  Destruct n; Auto.
+  NewDestruct m; Auto.
+  NewDestruct n; Auto.
   Intros. 
   Simpl in H. Discriminate H.
 Qed.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index ff502af94..f34c97d23 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -25,12 +25,12 @@ Proof.
 Red.
 Cut (n:nat)(a:A)(lt (f a) n)->(Acc A ltof a).
 Intros H a;  Apply (H (S (f a))); Auto with arith.
-Induction n.
+NewInduction n.
 Intros; Absurd (lt (f a) O); Auto with arith.
-Intros m Hm a ltSma.
+Intros a ltSma.
 Apply Acc_intro.
 Unfold ltof; Intros b ltfafb.
-Apply Hm.
+Apply IHn.
 Apply lt_le_trans with (f a); Auto with arith.
 Qed.
 
@@ -60,12 +60,12 @@ Theorem induction_ltof1
 Proof.
 Intros P F; Cut (n:nat)(a:A)(lt (f a) n)->(P a).
 Intros H a;  Apply (H (S (f a))); Auto with arith.
-Induction n.
+NewInduction n.
 Intros; Absurd (lt (f a) O); Auto with arith.
-Intros m Hm a ltSma.
+Intros a ltSma.
 Apply F.
 Unfold ltof; Intros b ltfafb.
-Apply Hm.
+Apply IHn.
 Apply lt_le_trans with (f a); Auto with arith.
 Qed. 
 
@@ -94,12 +94,12 @@ Proof.
 Red.
 Cut (n:nat)(a:A)(lt (f a) n)->(Acc A R a).
 Intros H a; Apply (H (S (f a))); Auto with arith.
-Induction n.
+NewInduction n.
 Intros; Absurd (lt (f a) O); Auto with arith.
-Intros m Hm a ltSma.
+Intros a ltSma.
 Apply Acc_intro.
 Intros b ltfafb.
-Apply Hm.
+Apply IHn.
 Apply lt_le_trans with (f a); Auto with arith.
 Save.
 
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 4f7df44fd..3c82fd8e9 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -57,7 +57,7 @@ Save.
 Hints Resolve eq_true_false_abs : bool.
 
 Lemma not_true_is_false : (b:bool)~b=true->b=false.
-Destruct b.
+NewDestruct b.
 Intros.
 Red in H; Elim H.
 Reflexivity.
@@ -66,7 +66,7 @@ Reflexivity.
 Save.
 
 Lemma not_false_is_true : (b:bool)~b=false->b=true.
-Destruct b.
+NewDestruct b.
 Intros.
 Reflexivity.
 Intro H; Red in H; Elim H.
@@ -98,19 +98,19 @@ Definition eqb : bool->bool->bool :=
     end.
 
 Lemma eqb_refl : (x:bool)(Is_true (eqb x x)).
-Destruct x; Simpl; Auto with bool.
+NewDestruct x; Simpl; Auto with bool.
 Save.
 
 Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y.
-Destruct x; Destruct y; Simpl; Tauto.
+NewDestruct x; NewDestruct y; Simpl; Tauto.
 Save.
 
 Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true.
-Destruct x; Simpl; Tauto.
+NewDestruct x; Simpl; Tauto.
 Save.
  
 Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
-Destruct x; Simpl; Auto with bool.
+NewDestruct x; Simpl; Auto with bool.
 Save.
 
 Lemma eqb_subst : 
@@ -137,7 +137,7 @@ Trivial with bool.
 Save.
 
 Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b.
-Destruct a; Destruct b; Simpl; Intro;
+NewDestruct a; NewDestruct b; Simpl; Intro;
   Discriminate H Orelse Reflexivity.
 Save.
 
@@ -190,13 +190,13 @@ Save.
 Lemma negb_orb : (b1,b2:bool)
   (negb (orb b1 b2)) = (andb (negb b1) (negb b2)).
 Proof.
-  Destruct b1; Destruct b2; Simpl; Reflexivity.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
 Qed.
 
 Lemma negb_andb : (b1,b2:bool)
   (negb (andb b1 b2)) = (orb (negb b1) (negb b2)).
 Proof.
-  Destruct b1; Destruct b2; Simpl; Reflexivity.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
 Qed.
 
 Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')).
@@ -210,13 +210,13 @@ Induction b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool.
 Save.
 
 Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false.
-Destruct b.
+NewDestruct b.
 Trivial with bool.
 Trivial with bool.
 Save.
  
 Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false.
-Destruct b.
+NewDestruct b.
 Trivial with bool.
 Trivial with bool.
 Save.
@@ -244,10 +244,10 @@ Save.
 
 Lemma orb_true_intro 
     : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true.
-Destruct b1; Auto with bool.
-Destruct 1; Intros.
+NewDestruct b1; Auto with bool.
+NewDestruct 1; Intros.
 Elim diff_true_false; Auto with bool.
-Rewrite H0; Trivial with bool.
+Rewrite H; Trivial with bool.
 Save.
 Hints Resolve orb_true_intro : bool v62.
 
@@ -261,7 +261,7 @@ Trivial with bool.
 Save.
 
 Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
-Destruct b1; [Auto with bool | Destruct b2; Auto with bool].
+NewDestruct b1; [Auto with bool | NewDestruct b2; Auto with bool].
 Save.
 Lemma orb_false_intro 
     : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
@@ -271,22 +271,22 @@ Hints Resolve orb_false_intro : bool v62.
 
 Lemma orb_b_false : (b:bool)(orb b false)=b.
 Proof.
-  Destruct b; Trivial with bool.
+  NewDestruct b; Trivial with bool.
 Save.
 Hints Resolve orb_b_false : bool v62.
 
 Lemma orb_false_b : (b:bool)(orb false b)=b.
 Proof.
-  Destruct b; Trivial with bool.
+  NewDestruct b; Trivial with bool.
 Save.
 Hints Resolve orb_false_b : bool v62.
 
 Lemma orb_false_elim : 
     (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false).
 Proof.
-  Destruct b1.
+  NewDestruct b1.
   Intros; Elim diff_true_false; Auto with bool.
-  Destruct b2.
+  NewDestruct b2.
   Intros; Elim diff_true_false; Auto with bool.
   Auto with bool.
 Save.
@@ -294,17 +294,17 @@ Save.
 Lemma orb_neg_b :
   (b:bool)(orb b (negb b))=true.
 Proof.
-  Destruct b; Reflexivity.
+  NewDestruct b; Reflexivity.
 Save.
 Hints Resolve orb_neg_b : bool v62.
 
 Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1).
-Destruct b1; Destruct b2; Reflexivity.
+NewDestruct b1; NewDestruct b2; Reflexivity.
 Save.
 
 Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3).
 Proof.
-  Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+  NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62.
@@ -332,29 +332,29 @@ Hints Resolve andb_prop2 : bool v62.
 
 Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true.
 Proof.
-  Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool.
+  NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
 Save.
 Hints Resolve andb_true_intro : bool v62.
 
 Lemma andb_true_intro2 : 
   (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)).
 Proof.
-  Destruct b1; Destruct b2; Simpl; Tauto.
+  NewDestruct b1; NewDestruct b2; Simpl; Tauto.
 Save.
 Hints Resolve andb_true_intro2 : bool v62.
 
 Lemma andb_false_intro1 
     : (b1,b2:bool)(b1=false)->(andb b1 b2)=false.
-Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool.
+NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
 Save.
 
 Lemma andb_false_intro2 
     : (b1,b2:bool)(b2=false)->(andb b1 b2)=false.
-Destruct b1; Destruct b2; Simpl; Tauto Orelse Auto with bool.
+NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
 Save.
 
 Lemma andb_b_false : (b:bool)(andb b false)=false.
-Destruct b; Auto with bool.
+NewDestruct b; Auto with bool.
 Save.
 
 Lemma andb_false_b : (b:bool)(andb false b)=false.
@@ -362,7 +362,7 @@ Trivial with bool.
 Save.
 
 Lemma andb_b_true : (b:bool)(andb b true)=b.
-Destruct b; Auto with bool.
+NewDestruct b; Auto with bool.
 Save.
 
 Lemma andb_true_b : (b:bool)(andb true b)=b.
@@ -371,22 +371,22 @@ Save.
 
 Lemma andb_false_elim : 
     (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
-Destruct b1; Destruct b2; Simpl; Auto with bool.
+NewDestruct b1; NewDestruct b2; Simpl; Auto with bool.
 Save.
 Hints Resolve andb_false_elim : bool v62.
 
 Lemma andb_neg_b :
    (b:bool)(andb b (negb b))=false.
-Destruct b; Reflexivity.
+NewDestruct b; Reflexivity.
 Save.   
 Hints Resolve andb_neg_b : bool v62.
 
 Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1).
-Destruct b1; Destruct b2; Reflexivity.
+NewDestruct b1; NewDestruct b2; Reflexivity.
 Save.
 
 Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3).
-Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Hints Resolve andb_sym andb_assoc : bool v62.
@@ -463,32 +463,32 @@ Qed.
 
 Lemma demorgan1 : (b1,b2,b3:bool)
   (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)).
-Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Lemma demorgan2 : (b1,b2,b3:bool)
   (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)).
-Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Lemma demorgan3 : (b1,b2,b3:bool)
   (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)).
-Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Lemma demorgan4 : (b1,b2,b3:bool)
   (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)).
-Destruct b1; Destruct b2; Destruct b3; Reflexivity.
+NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
 Save.
 
 Lemma absoption_andb : (b1,b2:bool)
   (andb b1 (orb b1 b2)) = b1.
 Proof.
-  Destruct b1; Destruct b2; Simpl; Reflexivity.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
 Qed.
 
 Lemma absoption_orb : (b1,b2:bool)
   (orb b1 (andb b1 b2)) = b1.
 Proof.
-  Destruct b1; Destruct b2; Simpl; Reflexivity.
+  NewDestruct b1; NewDestruct b2; Simpl; Reflexivity.
 Qed.
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index f9c5e3976..d0c089c7a 100755
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -17,12 +17,12 @@ Inductive IfProp [A,B:Prop] : bool-> Prop
 Hints Resolve Iftrue Iffalse : bool v62.
 
 Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
-Destruct 1; Intros; Auto with bool.
+NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Auto with bool.
 Save.
 
 Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
-Destruct 1; Intros; Auto with bool.
+NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Trivial with bool.
 Save.
 
@@ -39,11 +39,11 @@ Assumption.
 Save.
 
 Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
-Destruct 1; Auto with bool.
+NewDestruct 1; Auto with bool.
 Save.
 
 Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
-Destruct b; Intro H.
+NewDestruct b; Intro H.
 Left; Inversion H; Auto with bool.
 Right; Inversion H; Auto with bool.
 Save.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 8a8d09621..4422a03f4 100755
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -15,19 +15,19 @@ Definition zerob : nat->bool
       := [n:nat]Cases n of O => true | (S _) => false end.
 
 Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
-Destruct n; [Trivial with bool | Intros p H; Inversion H].
+NewDestruct n; [Trivial with bool | Inversion 1].
 Save.
 Hints Resolve zerob_true_intro : bool.
 
 Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
-Destruct n; [Trivial with bool | Intros p H; Inversion H].
+NewDestruct n; [Trivial with bool | Inversion 1].
 Save.
 
 Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
-Destruct n; [Destruct 1; Auto with bool | Trivial with bool].
+NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool].
 Save.
 Hints Resolve zerob_false_intro : bool.
 
 Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
-Destruct n; [Intro H; Inversion H | Auto with bool].
+NewDestruct n; [Intro H; Inversion H | Auto with bool].
 Save.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 2c5c0f569..8c3ade1cd 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -150,7 +150,7 @@ Section Logic_lemmas.
   Proof.
    Intros.
    Cut (identity A x y).
-   Destruct 1; Auto.
+   NewDestruct 1; Auto.
    Elim H; Auto.
   Qed.
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index eb7edad11..4882ea29c 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -189,7 +189,7 @@ Lemma False_rect: (C:Type)False->C.
 Proof.
   Intros.
   Cut Empty_set.
-  Destruct 1.
+  NewDestruct 1.
   Elim H.
 Qed.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 214c33117..bd55dcd1d 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -29,7 +29,7 @@ Chapter Well_founded.
     := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x).
 
  Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y).
-  Destruct 1; Trivial.
+  NewDestruct 1; Trivial.
  Defined.
 
   (* the informative elimination :
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 088b03845..a74dcf5b8 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -18,7 +18,7 @@ Inductive ad : Set :=
 
 Lemma ad_sum : (a:ad) {p:positive | a=(ad_x p)}+{a=ad_z}.
 Proof.
-  Destruct a; Auto.
+  NewDestruct a; Auto.
   Left; Exists p; Trivial.
 Qed.
 
@@ -74,15 +74,15 @@ Qed.
 
 Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a).
 Proof.
-  Destruct a; Destruct a'; Simpl; Auto.
-  Induction p; Simpl; Auto.
-  Destruct p0; Simpl; Trivial; Intros.
+  NewDestruct a; NewDestruct a'; Simpl; Auto.
+  Generalize p0; Clear p0; Induction p; Simpl; Auto.
+  NewDestruct p0; Simpl; Trivial; Intros.
   Rewrite Hrecp; Trivial.
   Rewrite Hrecp; Trivial.
-  Destruct p0; Simpl; Trivial; Intros.
+  NewDestruct p0; Simpl; Trivial; Intros.
   Rewrite Hrecp; Trivial.
   Rewrite Hrecp; Trivial.
-  Induction p; Simpl; Auto.
+  Induction p0; Simpl; Auto.
 Qed.
 
 Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z.
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index c1d07eaa6..7eeeb73f0 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -84,9 +84,9 @@ Qed.
 
 Lemma app_eq_nil: (x,y:list) (x^y)=nil -> x=nil /\ y=nil.
 Proof.
- Destruct x;Destruct y;Simpl;Auto.
+ NewDestruct x;NewDestruct y;Simpl;Auto.
  Intros H;Discriminate H.
- Intros a0 l0 H;Discriminate H.
+ Intros;Discriminate H.
 Qed.
 
 Lemma app_cons_not_nil: (x,y:list)(a:A)~nil=(x^(cons a y)).
@@ -101,7 +101,7 @@ Lemma app_eq_unit:(x,y:list)(a:A)
      (x^y)=(cons a nil)-> (x=nil)/\ y=(cons a nil) \/ x=(cons a nil)/\ y=nil.
 
 Proof.
- Destruct x;Destruct y;Simpl.
+ NewDestruct x;NewDestruct y;Simpl.
  Intros a H;Discriminate H.
  Left;Split;Auto.
  Right;Split;Auto.
@@ -442,7 +442,7 @@ i*)
 
 Lemma list_eq_dec : ((x,y:A){x=y}+{~x=y})->(x,y:list){x=y}+{~x=y}.
 Proof.
-  Induction x; Destruct y; Intros; Auto.
+  Induction x; NewDestruct y; Intros; Auto.
   Case (H a a0); Intro e.
   Case (H0 l0); Intro e'.
   Left; Rewrite e; Rewrite e'; Trivial.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 0bee9226e..41ef49eaa 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -17,14 +17,14 @@ Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop :=
 Hints Resolve JMeq_refl.
 
 Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
-Destruct 1; Trivial.
+NewDestruct 1; Trivial.
 Save.
 
 Hints Immediate JMeq_sym.
 
 Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C)
 	(JMeq x y)->(JMeq y z)->(JMeq x z).
-Destruct 1; Trivial.
+NewDestruct 1; Trivial.
 Save.
 
 Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index a9c26fa72..3a1d677db 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -105,12 +105,12 @@ Hints Resolve Rlt_le : real.
 
 (**********)
 Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``.
-Destruct 1; Red; Auto with real.
+NewDestruct 1; Red; Auto with real.
 Save.
 
 (**********)
 Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``.
-Destruct 1; Red; Auto with real.
+NewDestruct 1; Red; Auto with real.
 Save.
 
 (**********)
@@ -1355,7 +1355,7 @@ Save.
 
 (**********)
 Lemma plus_IZR:(z,t:Z)(IZR `z+t`)==``(IZR z)+(IZR t)``.
-Destruct z; Destruct t; Intros; Auto with real.
+NewDestruct z; NewDestruct t; Intros; Auto with real.
 Simpl; Intros; Rewrite convert_add; Auto with real.
 Apply plus_IZR_NEG_POS.
 Rewrite Zplus_sym; Rewrite Rplus_sym; Apply plus_IZR_NEG_POS.
@@ -1406,7 +1406,7 @@ Save.
 
 (**********)
 Lemma eq_IZR_R0:(z:Z)``(IZR z)==0``->`z=0`.
-Destruct z; Simpl; Intros; Auto with zarith.
+NewDestruct z; Simpl; Intros; Auto with zarith.
 Case (Rlt_not_eq ``0`` (INR (convert p))); Auto with real.
 Case (Rlt_not_eq ``-(INR (convert p))`` ``0`` ); Auto with real.
 Save.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 104b8b437..01b442a85 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -146,7 +146,7 @@ Proof.
  Intros.
  Inversion_clear H.
  Apply Acc_intro.
- Destruct y0;Intros.
+ NewDestruct y0;Intros.
  Inversion_clear H;Inversion_clear H1;Apply H0.
  Apply sp_swap.
  Apply right_sym;Auto with sets.
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.