Kills the useless tactic annotations "in |- *"

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

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

16 files changed, 90 insertions, 90 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 67039072b..69dded848 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -74,7 +74,7 @@ Section Between.
 
   Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r.
   Proof.
-    red in |- *; auto with arith.
+    red; auto with arith.
   Qed.
   Hint Resolve in_int_intro: arith v62.
 
@@ -149,7 +149,7 @@ Section Between.
       between k l ->
       (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
   Proof.
-    induction 1; red in |- *; intros.
+    induction 1; red; intros.
     absurd (k < k); auto with arith.
     absurd (Q l); auto with arith.
     elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index dc4da448e..d304b99bd 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -39,7 +39,7 @@ Proof.
   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.
-  right; exists (n - S (S m)); simpl in |- *.
+  right; exists (n - S (S m)); simpl.
   rewrite (plus_comm m (n - S (S m))).
   rewrite (plus_n_Sm (n - S (S m)) m).
   rewrite (plus_n_Sm (n - S (S m)) (S m)).
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 1cb91f9a5..f6801da20 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -256,7 +256,7 @@ Lemma leb_correct : forall m n, m <= n -> leb m n = true.
 Proof.
   induction m as [| m IHm]. trivial.
   destruct n. intro H. elim (le_Sn_O _ H).
-  intros. simpl in |- *. apply IHm. apply le_S_n. assumption.
+  intros. simpl. apply IHm. apply le_S_n. assumption.
 Qed.
 
 Lemma leb_complete : forall m n, leb m n = true -> m <= n.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index da1d9e989..68652b70c 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -43,7 +43,7 @@ Qed.
 
 Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
 Proof.
-  intro n. pattern n in |- *. apply ind_0_1_SS.
+  intro n. pattern n. apply ind_0_1_SS.
   (* n = 0 *)
   inversion 1.
   (* n=1 *)
@@ -99,12 +99,12 @@ Hint Unfold double: arith.
 
 Lemma double_S : forall n, double (S n) = S (S (double n)).
 Proof.
-  intro. unfold double in |- *. simpl in |- *. auto with arith.
+  intro. unfold double. simpl. auto with arith.
 Qed.
 
 Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
 Proof.
-  intros m n. unfold double in |- *.
+  intros m n. unfold double.
   do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
   reflexivity.
 Qed.
@@ -115,7 +115,7 @@ Lemma even_odd_double :
   forall n,
     (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 Proof.
-  intro n. pattern n in |- *. apply ind_0_1_SS.
+  intro n. pattern n. apply ind_0_1_SS.
   (* n = 0 *)
   split; split; auto with arith.
   intro H. inversion H.
@@ -126,11 +126,11 @@ Proof.
   intros. destruct H as ((IH1,IH2),(IH3,IH4)).
   split; split.
   intro H. inversion H. inversion H1.
-  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  simpl. rewrite (double_S (div2 n0)). auto with arith.
+  simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
   intro H. inversion H. inversion H1.
-  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
-  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
+  simpl. rewrite (double_S (div2 n0)). auto with arith.
+  simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 Qed.
 (** Specializations *)
 
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 1dc69f612..331990c54 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -23,7 +23,7 @@ Fixpoint eq_nat n m : Prop :=
   end.
 
 Theorem eq_nat_refl : forall n, eq_nat n n.
-  induction n; simpl in |- *; auto.
+  induction n; simpl; auto.
 Qed.
 Hint Resolve eq_nat_refl: arith v62.
 
@@ -35,7 +35,7 @@ Qed.
 Hint Immediate eq_eq_nat: arith v62.
 
 Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m.
-  induction n; induction m; simpl in |- *; contradiction || auto with arith.
+  induction n; induction m; simpl; contradiction || auto with arith.
 Qed.
 Hint Immediate eq_nat_eq: arith v62.
 
@@ -55,11 +55,11 @@ Proof.
   induction n.
   destruct m as [| n].
   auto with arith.
-  intros; right; red in |- *; trivial with arith.
+  intros; right; red; trivial with arith.
   destruct m as [| n0].
-  right; red in |- *; auto with arith.
+  right; red; auto with arith.
   intros.
-  simpl in |- *.
+  simpl.
   apply IHn.
 Defined.
 
@@ -76,12 +76,12 @@ Fixpoint beq_nat n m : bool :=
 
 Lemma beq_nat_refl : forall n, true = beq_nat n n.
 Proof.
-  intro x; induction x; simpl in |- *; auto.
+  intro x; induction x; simpl; auto.
 Qed.
 
 Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y.
 Proof.
-  double induction x y; simpl in |- *.
+  double induction x y; simpl.
     reflexivity.
     intros n H1 H2. discriminate H2.
     intros n H1 H2. discriminate H2.
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 513fd1108..6dd0272a8 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -19,16 +19,16 @@ Inductive diveucl a b : Set :=
 
 Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n.
 Proof.
-  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  intros b H a; pattern a; apply gt_wf_rec; intros n H0.
   elim (le_gt_dec b n).
   intro lebn.
   elim (H0 (n - b)); auto with arith.
   intros q r g e.
-  apply divex with (S q) r; simpl in |- *; auto with arith.
+  apply divex with (S q) r; simpl; auto with arith.
   elim plus_assoc.
   elim e; auto with arith.
   intros gtbn.
-  apply divex with 0 n; simpl in |- *; auto with arith.
+  apply divex with 0 n; simpl; auto with arith.
 Defined.
 
 Lemma quotient :
@@ -36,17 +36,17 @@ Lemma quotient :
     n > 0 ->
     forall m:nat, {q : nat |  exists r : nat, m = q * n + r /\ n > r}.
 Proof.
-  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  intros b H a; pattern a; apply gt_wf_rec; intros n H0.
   elim (le_gt_dec b n).
   intro lebn.
   elim (H0 (n - b)); auto with arith.
   intros q Hq; exists (S q).
   elim Hq; intros r Hr.
-  exists r; simpl in |- *; elim Hr; intros.
+  exists r; simpl; elim Hr; intros.
   elim plus_assoc.
   elim H1; auto with arith.
   intros gtbn.
-  exists 0; exists n; simpl in |- *; auto with arith.
+  exists 0; exists n; simpl; auto with arith.
 Defined.
 
 Lemma modulo :
@@ -54,15 +54,15 @@ Lemma modulo :
     n > 0 ->
     forall m:nat, {r : nat |  exists q : nat, m = q * n + r /\ n > r}.
 Proof.
-  intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0.
+  intros b H a; pattern a; apply gt_wf_rec; intros n H0.
   elim (le_gt_dec b n).
   intro lebn.
   elim (H0 (n - b)); auto with arith.
   intros r Hr; exists r.
   elim Hr; intros q Hq.
-  elim Hq; intros; exists (S q); simpl in |- *.
+  elim Hq; intros; exists (S q); simpl.
   elim plus_assoc.
   elim H1; auto with arith.
   intros gtbn.
-  exists n; exists 0; simpl in |- *; auto with arith.
+  exists n; exists 0; simpl; auto with arith.
 Defined.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 9a84a7f2e..23dc1d259 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -145,7 +145,7 @@ Lemma even_mult_aux :
   forall n m,
     (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m).
 Proof.
-  intros n; elim n; simpl in |- *; auto with arith.
+  intros n; elim n; simpl; auto with arith.
   intros m; split; split; auto with arith.
   intros H'; inversion H'.
   intros H'; elim H'; auto.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index 82643cdcd..1432995e3 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -23,7 +23,7 @@ Arguments fact n%nat.
 
 Lemma lt_O_fact : forall n:nat, 0 < fact n.
 Proof.
-  simple induction n; unfold lt in |- *; simpl in |- *; auto with arith.
+  simple induction n; unfold lt; simpl; auto with arith.
 Qed.
 
 Lemma fact_neq_0 : forall n:nat, fact n <> 0.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index f9bf0f2fd..04d44f9c9 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -47,7 +47,7 @@ Hint Immediate gt_S_n: arith v62.
 
 Theorem gt_S : forall n m, S n > m -> n > m \/ m = n.
 Proof.
-  intros n m H; unfold gt in |- *; apply le_lt_or_eq; auto with arith.
+  intros n m H; unfold gt; apply le_lt_or_eq; auto with arith.
 Qed.
 
 Lemma gt_pred : forall n m, m > S n -> pred m > n.
@@ -110,23 +110,23 @@ Hint Resolve le_gt_S: arith v62.
 
 Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p.
 Proof.
-  red in |- *; intros; apply lt_le_trans with m; auto with arith.
+  red; intros; apply lt_le_trans with m; auto with arith.
 Qed.
 
 Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p.
 Proof.
-  red in |- *; intros; apply le_lt_trans with m; auto with arith.
+  red; intros; apply le_lt_trans with m; auto with arith.
 Qed.
 
 Lemma gt_trans : forall n m p, n > m -> m > p -> n > p.
 Proof.
-  red in |- *; intros n m p H1 H2.
+  red; intros n m p H1 H2.
   apply lt_trans with m; auto with arith.
 Qed.
 
 Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p.
 Proof.
-  red in |- *; intros; apply lt_le_trans with m; auto with arith.
+  red; intros; apply lt_le_trans with m; auto with arith.
 Qed.
 
 Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
@@ -142,7 +142,7 @@ Qed.
 
 Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m.
 Proof.
-  red in |- *; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
+  red; intros n m p H; apply plus_lt_reg_l with p; auto with arith.
 Qed.
 
 Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 717705a1c..35d200055 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -46,8 +46,8 @@ Qed.
 
 Theorem le_Sn_0 : forall n, ~ S n <= 0.
 Proof.
-  red in |- *; intros n H.
-  change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
+  red; intros n H.
+  change (IsSucc 0); elim H; simpl; auto with arith.
 Qed.
 
 Hint Resolve le_0_n le_Sn_0: arith v62.
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 1f7e6e018..940448202 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -51,7 +51,7 @@ Qed.
 
 Theorem lt_not_le : forall n m, n < m -> ~ m <= n.
 Proof.
-  red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt).
+  red; intros n m Lt Le; exact (le_not_lt m n Le Lt).
 Qed.
 Hint Immediate le_not_lt lt_not_le: arith v62.
 
@@ -107,12 +107,12 @@ Qed.
 
 Lemma lt_pred : forall n m, S n < m -> n < pred m.
 Proof.
-induction 1; simpl in |- *; auto with arith.
+induction 1; simpl; auto with arith.
 Qed.
 Hint Immediate lt_pred: arith v62.
 
 Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n.
-destruct 1; simpl in |- *; auto with arith.
+destruct 1; simpl; auto with arith.
 Qed.
 Hint Resolve lt_pred_n_n: arith v62.
 
@@ -159,7 +159,7 @@ Hint Immediate lt_le_weak: arith v62.
 
 Theorem le_or_lt : forall n m, n <= m \/ m < n.
 Proof.
-  intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith.
+  intros n m; pattern n, m; apply nat_double_ind; auto with arith.
   induction 1; auto with arith.
 Qed.
 
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 7ec37a65e..85ac944cd 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -29,7 +29,7 @@ Implicit Types m n p : nat.
 
 Lemma minus_n_O : forall n, n = n - 0.
 Proof.
-  induction n; simpl in |- *; auto with arith.
+  induction n; simpl; auto with arith.
 Qed.
 Hint Resolve minus_n_O: arith v62.
 
@@ -37,21 +37,21 @@ Hint Resolve minus_n_O: arith v62.
 
 Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
 Proof.
-  intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
+  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
     auto with arith.
 Qed.
 Hint Resolve minus_Sn_m: arith v62.
 
 Theorem pred_of_minus : forall n, pred n = n - 1.
 Proof.
-  intro x; induction x; simpl in |- *; auto with arith.
+  intro x; induction x; simpl; auto with arith.
 Qed.
 
 (** * Diagonal *)
 
 Lemma minus_diag : forall n, n - n = 0.
 Proof.
-  induction n; simpl in |- *; auto with arith.
+  induction n; simpl; auto with arith.
 Qed.
 
 Lemma minus_diag_reverse : forall n, 0 = n - n.
@@ -66,7 +66,7 @@ Notation minus_n_n := minus_diag_reverse.
 
 Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
 Proof.
-  induction p; simpl in |- *; auto with arith.
+  induction p; simpl; auto with arith.
 Qed.
 Hint Resolve minus_plus_simpl_l_reverse: arith v62.
 
@@ -74,7 +74,7 @@ Hint Resolve minus_plus_simpl_l_reverse: arith v62.
 
 Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
 Proof.
-  intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *;
+  intros n m p; pattern m, n; apply nat_double_ind; simpl;
     intros.
   replace (n0 - 0) with n0; auto with arith.
   absurd (0 = S (n0 + p)); auto with arith.
@@ -83,20 +83,20 @@ Qed.
 Hint Immediate plus_minus: arith v62.
 
 Lemma minus_plus : forall n m, n + m - n = m.
-  symmetry  in |- *; auto with arith.
+  symmetry ; auto with arith.
 Qed.
 Hint Resolve minus_plus: arith v62.
 
 Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
 Proof.
-  intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *;
+  intros n m Le; pattern n, m; apply le_elim_rel; simpl;
     auto with arith.
 Qed.
 Hint Resolve le_plus_minus: arith v62.
 
 Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
 Proof.
-  symmetry  in |- *; auto with arith.
+  symmetry ; auto with arith.
 Qed.
 Hint Resolve le_plus_minus_r: arith v62.
 
@@ -132,7 +132,7 @@ Qed.
 
 Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
-  intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
+  intros n m Le; pattern m, n; apply le_elim_rel; simpl;
     auto using le_minus with arith.
     intros; absurd (0 < 0); auto with arith.
 Qed.
@@ -140,7 +140,7 @@ Hint Resolve lt_minus: arith v62.
 
 Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n.
 Proof.
-  intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *;
+  intros n m; pattern n, m; apply nat_double_ind; simpl;
     auto with arith.
   intros; absurd (0 < 0); trivial with arith.
 Qed.
@@ -148,9 +148,9 @@ Hint Immediate lt_O_minus_lt: arith v62.
 
 Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
 Proof.
-  intros y x; pattern y, x in |- *; apply nat_double_ind;
-    [ simpl in |- *; trivial with arith
+  intros y x; pattern y, x; apply nat_double_ind;
+    [ simpl; trivial with arith
       | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
-      | simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3;
+      | simpl; intros n m H1 H2; apply H1; unfold not; intros H3;
 	apply H2; apply le_n_S; assumption ].
 Qed.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 64b0d4dd3..0c44cfaf1 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -23,7 +23,7 @@ Implicit Types m n p : nat.
 
 Lemma mult_0_r : forall n, n * 0 = 0.
 Proof.
-  intro; symmetry  in |- *; apply mult_n_O.
+  intro; symmetry ; apply mult_n_O.
 Qed.
 
 Lemma mult_0_l : forall n, 0 * n = 0.
@@ -35,7 +35,7 @@ Qed.
 
 Lemma mult_1_l : forall n, 1 * n = n.
 Proof.
-  simpl in |- *; auto with arith.
+  simpl; auto with arith.
 Qed.
 Hint Resolve mult_1_l: arith v62.
 
@@ -68,7 +68,7 @@ Hint Resolve mult_plus_distr_r: arith v62.
 Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.
 Proof.
   induction n. trivial.
-  intros. simpl in |- *. rewrite IHn. symmetry. apply plus_permute_2_in_4.
+  intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4.
 Qed.
 
 Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p.
@@ -137,13 +137,13 @@ Qed.
 
 Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
 Proof.
-  induction m; simpl in |- *; auto with arith.
+  induction m; simpl; auto with arith.
 Qed.
 Hint Resolve mult_O_le: arith v62.
 
 Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
 Proof.
-  induction p as [| p IHp]; intros; simpl in |- *.
+  induction p as [| p IHp]; intros; simpl.
   apply le_n.
   auto using plus_le_compat.
 Qed.
@@ -167,7 +167,7 @@ Proof.
   assumption.
   apply le_plus_l.
   (* m*p<=m0*q -> m*p<=(S m0)*q *)
-  simpl in |- *; apply le_trans with (m0 * q).
+  simpl; apply le_trans with (m0 * q).
   assumption.
   apply le_plus_r.
 Qed.
@@ -232,7 +232,7 @@ Fixpoint mult_acc (s:nat) m n : nat :=
 
 Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
 Proof.
-  induction n as [| p IHp]; simpl in |- *; auto.
+  induction n as [| p IHp]; simpl; auto.
   intros s m; rewrite <- plus_tail_plus; rewrite <- IHp.
   rewrite <- plus_assoc_reverse; apply f_equal2; auto.
   rewrite plus_comm; auto.
@@ -242,7 +242,7 @@ Definition tail_mult n m := mult_acc 0 m n.
 
 Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.
 Proof.
-  intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto.
+  intros; unfold tail_mult; rewrite <- mult_acc_aux; auto.
 Qed.
 
 (** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus]
@@ -250,4 +250,4 @@ Qed.
 
 Ltac tail_simpl :=
   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
-    simpl in |- *.
+    simpl.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index e68ba9590..e121ce30d 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -29,7 +29,7 @@ Defined.
 Hint Resolve O_or_S eq_nat_dec: arith.
 
 Theorem dec_eq_nat : forall n m, decidable (n = m).
-  intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
+  intros x y; unfold decidable; elim (eq_nat_dec x y); auto with arith.
 Defined.
 
 Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index c036d06e1..5428ada32 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -33,7 +33,7 @@ Definition plus_0_r n := eq_sym (plus_n_O n).
 
 Lemma plus_comm : forall n m, n + m = m + n.
 Proof.
-  intros n m; elim n; simpl in |- *; auto with arith.
+  intros n m; elim n; simpl; auto with arith.
   intros y H; elim (plus_n_Sm m y); auto with arith.
 Qed.
 Hint Immediate plus_comm: arith v62.
@@ -45,7 +45,7 @@ Definition plus_Snm_nSm : forall n m, S n + m = n + S m:=
 
 Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
 Proof.
-  intros n m p; elim n; simpl in |- *; auto with arith.
+  intros n m p; elim n; simpl; auto with arith.
 Qed.
 Hint Resolve plus_assoc: arith v62.
 
@@ -64,42 +64,42 @@ Hint Resolve plus_assoc_reverse: arith v62.
 
 Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m.
 Proof.
-  intros m p n; induction n; simpl in |- *; auto with arith.
+  intros m p n; induction n; simpl; auto with arith.
 Qed.
 
 Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m.
 Proof.
-  induction p; simpl in |- *; auto with arith.
+  induction p; simpl; auto with arith.
 Qed.
 
 Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m.
 Proof.
-  induction p; simpl in |- *; auto with arith.
+  induction p; simpl; auto with arith.
 Qed.
 
 (** * Compatibility with order *)
 
 Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.
 Proof.
-  induction p; simpl in |- *; auto with arith.
+  induction p; simpl; auto with arith.
 Qed.
 Hint Resolve plus_le_compat_l: arith v62.
 
 Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p.
 Proof.
-  induction 1; simpl in |- *; auto with arith.
+  induction 1; simpl; auto with arith.
 Qed.
 Hint Resolve plus_le_compat_r: arith v62.
 
 Lemma le_plus_l : forall n m, n <= n + m.
 Proof.
-  induction n; simpl in |- *; auto with arith.
+  induction n; simpl; auto with arith.
 Qed.
 Hint Resolve le_plus_l: arith v62.
 
 Lemma le_plus_r : forall n m, m <= n + m.
 Proof.
-  intros n m; elim n; simpl in |- *; auto with arith.
+  intros n m; elim n; simpl; auto with arith.
 Qed.
 Hint Resolve le_plus_r: arith v62.
 
@@ -117,7 +117,7 @@ Hint Immediate lt_plus_trans: arith v62.
 
 Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
 Proof.
-  induction p; simpl in |- *; auto with arith.
+  induction p; simpl; auto with arith.
 Qed.
 Hint Resolve plus_lt_compat_l: arith v62.
 
@@ -131,18 +131,18 @@ Hint Resolve plus_lt_compat_r: arith v62.
 Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q.
 Proof.
   intros n m p q H H0.
-  elim H; simpl in |- *; auto with arith.
+  elim H; simpl; auto with arith.
 Qed.
 
 Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q.
 Proof.
-  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. rewrite plus_Snm_nSm.
+  unfold lt. intros. change (S n + p <= m + q). rewrite plus_Snm_nSm.
   apply plus_le_compat; assumption.
 Qed.
 
 Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q.
 Proof.
-  unfold lt in |- *. intros. change (S n + p <= m + q) in |- *. apply plus_le_compat; assumption.
+  unfold lt. intros. change (S n + p <= m + q). apply plus_le_compat; assumption.
 Qed.
 
 Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
@@ -190,8 +190,8 @@ Fixpoint tail_plus n m : nat :=
   end.
 
 Lemma plus_tail_plus : forall n m, n + m = tail_plus n m.
-induction n as [| n IHn]; simpl in |- *; auto.
-intro m; rewrite <- IHn; simpl in |- *; auto.
+induction n as [| n IHn]; simpl; auto.
+intro m; rewrite <- IHn; simpl; auto.
 Qed.
 
 (** * Discrimination *)
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e264ccb5d..e579010ba 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -24,14 +24,14 @@ Definition gtof (a b:A) := f b > f a.
 
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
-  red in |- *.
+  red.
   cut (forall n (a:A), f a < n -> Acc ltof a).
   intros H a; apply (H (S (f a))); auto with arith.
   induction n.
   intros; absurd (f a < 0); auto with arith.
   intros a ltSma.
   apply Acc_intro.
-  unfold ltof in |- *; intros b ltfafb.
+  unfold ltof; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
 Defined.
@@ -73,7 +73,7 @@ Proof.
   intros; absurd (f a < 0); auto with arith.
   intros a ltSma.
   apply F.
-  unfold ltof in |- *; intros b ltfafb.
+  unfold ltof; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
 Defined.
@@ -108,7 +108,7 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-  red in |- *.
+  red.
   cut (forall n (a:A), f a < n -> Acc R a).
   intros H a; apply (H (S (f a))); auto with arith.
   induction n.
@@ -161,8 +161,8 @@ Lemma lt_wf_double_rec :
      (forall p q, p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-  intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
-  intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
+  intros P Hrec p; pattern p; apply lt_wf_rec.
+  intros n H q; pattern q; apply lt_wf_rec; auto with arith.
 Defined.
 
 Lemma lt_wf_double_ind :
@@ -171,8 +171,8 @@ Lemma lt_wf_double_ind :
       (forall p (q:nat), p < n -> P p q) ->
       (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-  intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
-  intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
+  intros P Hrec p; pattern p; apply lt_wf_ind.
+  intros n H q; pattern q; apply lt_wf_ind; auto with arith.
 Qed.
 
 Hint Resolve lt_wf: arith.
@@ -190,7 +190,7 @@ Section LT_WF_REL.
   Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
   Proof.
     intros x [n fxn]; generalize dependent x.
-    pattern n in |- *; apply lt_wf_ind; intros.
+    pattern n; apply lt_wf_ind; intros.
     constructor; intros.
     destruct (F_compat y x) as (x0,H1,H2); trivial.
     apply (H x0); auto.