5 files changed, 11 insertions, 11 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 5828fc3f8b..2966125935 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -72,7 +72,7 @@ Hint Resolve andb_prop: bool.
 Lemma andb_true_intro :
   forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
-  destruct b1; destruct b2; simpl in |- *; intros [? ?]; assumption.
+  destruct b1; destruct b2; simpl; intros [? ?]; assumption.
 Qed.
 Hint Resolve andb_true_intro: bool.
 
@@ -203,7 +203,7 @@ Lemma injective_projections :
   forall (A B:Type) (p1 p2:A * B),
     fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
 Proof.
-  destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
+  destruct p1; destruct p2; simpl; intros Hfst Hsnd.
   rewrite Hfst; rewrite Hsnd; reflexivity.
 Qed.
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 1dc998cdf4..50a715988a 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -261,12 +261,12 @@ Section universal_quantification.
 
   Theorem inst : forall x:A, all (fun x => P x) -> P x.
   Proof.
-    unfold all in |- *; auto.
+    unfold all; auto.
   Qed.
 
   Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P.
   Proof.
-    red in |- *; auto.
+    red; auto.
   Qed.
 
 End universal_quantification.
@@ -305,7 +305,7 @@ Section Logic_lemmas.
 
   Theorem absurd : forall A C:Prop, A -> ~ A -> C.
   Proof.
-    unfold not in |- *; intros A C h1 h2.
+    unfold not; intros A C h1 h2.
     destruct (h2 h1).
   Qed.
 
@@ -334,7 +334,7 @@ Section Logic_lemmas.
 
     Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
-      red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
+      red; intros h1 h2; apply h1; destruct h2; trivial.
     Qed.
 
   End equality.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index c244ac24f1..e501ac5273 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -44,7 +44,7 @@ Section identity_is_a_congruence.
 
  Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
  Proof.
-  red in |- *; intros H H'; apply H; destruct H'; trivial.
+  red; intros H H'; apply H; destruct H'; trivial.
  Qed.
 
 End identity_is_a_congruence.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index cbb960ceb4..4db490e282 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -54,7 +54,7 @@ Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
-  red in |- *; auto.
+  red; auto.
 Qed.
 Hint Resolve not_eq_S: core.
 
@@ -93,7 +93,7 @@ Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
-  induction n; simpl in |- *; auto.
+  induction n; simpl; auto.
 Qed.
 Hint Resolve plus_n_O: core.
 
@@ -104,7 +104,7 @@ Qed.
 
 Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
-  intros n m; induction n; simpl in |- *; auto.
+  intros n m; induction n; simpl; auto.
 Qed.
 Hint Resolve plus_n_Sm: core.
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 2bb7eae94a..df1a9df679 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -103,7 +103,7 @@ Section Well_founded.
 
   Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
   Proof.
-   intro x; unfold Fix in |- *.
+   intro x; unfold Fix.
    rewrite <- Fix_F_eq.
    apply F_ext; intros.
    apply Fix_F_inv.