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, 158 insertions, 158 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index f93631c7e..bf7b52b22 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -38,8 +38,8 @@ Section Ensembles_classical.
     elim (not_all_ex_not U (fun x:U => ~ In U A x)).
     intros x H; apply Inhabited_intro with x.
     apply NNPP; auto with sets.
-    red in |- *; intro.
-    apply NI; red in |- *.
+    red; intro.
+    apply NI; red.
     intros x H'; elim (H x); trivial with sets.
   Qed.
 
@@ -47,7 +47,7 @@ Section Ensembles_classical.
     forall A:Ensemble U, A <> Empty_set U -> Inhabited U A.
   Proof.
     intros; apply not_included_empty_Inhabited.
-    red in |- *; auto with sets.
+    red; auto with sets.
   Qed.
 
   Lemma Inhabited_Setminus :
@@ -73,7 +73,7 @@ Section Ensembles_classical.
   Lemma Subtract_intro :
     forall (A:Ensemble U) (x y:U), In U A y -> x <> y -> In U (Subtract U A x) y.
   Proof.
-    unfold Subtract at 1 in |- *; auto with sets.
+    unfold Subtract at 1; auto with sets.
   Qed.
   Hint Resolve Subtract_intro : sets.
 
@@ -103,7 +103,7 @@ Section Ensembles_classical.
   Lemma not_SIncl_empty :
     forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
   Proof.
-    intro X; red in |- *; intro H'; try exact H'.
+    intro X; red; intro H'; try exact H'.
     lapply (Strict_Included_inv X (Empty_set U)); auto with sets.
     intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0.
     intros x H'0; elim H'0.
@@ -113,10 +113,10 @@ Section Ensembles_classical.
   Lemma Complement_Complement :
     forall A:Ensemble U, Complement U (Complement U A) = A.
   Proof.
-    unfold Complement in |- *; intros; apply Extensionality_Ensembles;
+    unfold Complement; intros; apply Extensionality_Ensembles;
       auto with sets.
-    red in |- *; split; auto with sets.
-    red in |- *; intros; apply NNPP; auto with sets.
+    red; split; auto with sets.
+    red; intros; apply NNPP; auto with sets.
   Qed.
 
 End Ensembles_classical.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index e6dd83810..324255f6d 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -36,24 +36,24 @@ Section Ensembles_facts.
 
   Lemma Noone_in_empty : forall x:U, ~ In U (Empty_set U) x.
   Proof.
-    red in |- *; destruct 1.
+    red; destruct 1.
   Qed.
 
   Lemma Included_Empty : forall A:Ensemble U, Included U (Empty_set U) A.
   Proof.
-    intro; red in |- *.
+    intro; red.
     intros x H; elim (Noone_in_empty x); auto with sets.
   Qed.
 
   Lemma Add_intro1 :
     forall (A:Ensemble U) (x y:U), In U A y -> In U (Add U A x) y.
   Proof.
-    unfold Add at 1 in |- *; auto with sets.
+    unfold Add at 1; auto with sets.
   Qed.
 
   Lemma Add_intro2 : forall (A:Ensemble U) (x:U), In U (Add U A x) x.
   Proof.
-    unfold Add at 1 in |- *; auto with sets.
+    unfold Add at 1; auto with sets.
   Qed.
 
   Lemma Inhabited_add : forall (A:Ensemble U) (x:U), Inhabited U (Add U A x).
@@ -66,7 +66,7 @@ Section Ensembles_facts.
     forall X:Ensemble U, Inhabited U X -> X <> Empty_set U.
   Proof.
     intros X H'; elim H'.
-    intros x H'0; red in |- *; intro H'1.
+    intros x H'0; red; intro H'1.
     absurd (In U X x); auto with sets.
     rewrite H'1; auto using Noone_in_empty with sets.
   Qed.
@@ -78,7 +78,7 @@ Section Ensembles_facts.
 
   Lemma not_Empty_Add : forall (A:Ensemble U) (x:U), Empty_set U <> Add U A x.
   Proof.
-    intros; red in |- *; intro H; generalize (Add_not_Empty A x); auto with sets.
+    intros; red; intro H; generalize (Add_not_Empty A x); auto with sets.
   Qed.
 
   Lemma Singleton_inv : forall x y:U, In U (Singleton U x) y -> x = y.
@@ -121,7 +121,7 @@ Section Ensembles_facts.
     forall (A B:Ensemble U) (x:U),
       In U A x -> ~ In U B x -> In U (Setminus U A B) x.
   Proof.
-    unfold Setminus at 1 in |- *; red in |- *; auto with sets.
+    unfold Setminus at 1; red; auto with sets.
   Qed.
 
   Lemma Strict_Included_intro :
@@ -132,7 +132,7 @@ Section Ensembles_facts.
 
   Lemma Strict_Included_strict : forall X:Ensemble U, ~ Strict_Included U X X.
   Proof.
-    intro X; red in |- *; intro H'; elim H'.
+    intro X; red; intro H'; elim H'.
     intros H'0 H'1; elim H'1; auto with sets.
   Qed.
 
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f08436754..07543276b 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -61,7 +61,7 @@ Section Ensembles_finis_facts.
             (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n)
       end.
   Proof.
-    induction 1; simpl in |- *; auto.
+    induction 1; simpl; auto.
     exists A; exists x; auto.
   Qed.
 
@@ -73,7 +73,7 @@ Section Ensembles_finis_facts.
 	| S n => Inhabited U X
       end.
   Proof.
-    intros X p C; elim C; simpl in |- *; trivial with sets.
+    intros X p C; elim C; simpl; trivial with sets.
   Qed.
 
 End Ensembles_finis_facts.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 350cd783c..8895e4569 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -62,7 +62,7 @@ Section Finite_sets_facts.
   Theorem Singleton_is_finite : forall x:U, Finite U (Singleton U x).
   Proof.
     intro x; rewrite <- (Empty_set_zero U (Singleton U x)).
-    change (Finite U (Add U (Empty_set U) x)) in |- *; auto with sets.
+    change (Finite U (Add U (Empty_set U) x)); auto with sets.
   Qed.
 
   Theorem Union_preserves_Finite :
@@ -134,15 +134,15 @@ Section Finite_sets_facts.
     cut (S (pred n) = pred (S n)).
     intro H'5; rewrite <- H'5.
     apply card_add; auto with sets.
-    red in |- *; intro H'6; elim H'6.
+    red; intro H'6; elim H'6.
     intros H'7 H'8; try assumption.
     elim H'1; auto with sets.
-    unfold pred at 2 in |- *; symmetry  in |- *.
+    unfold pred at 2; symmetry .
     apply S_pred with (m := 0).
-    change (n > 0) in |- *.
+    change (n > 0).
     apply inh_card_gt_O with (X := X); auto with sets.
     apply Inhabited_intro with (x := x0); auto with sets.
-    red in |- *; intro H'3.
+    red; intro H'3.
     apply H'1.
     elim H'3; auto with sets.
     rewrite H'3; auto with sets.
@@ -152,7 +152,7 @@ Section Finite_sets_facts.
     intro H'4; rewrite H'4; auto with sets.
     intros H'3 H'4; try assumption.
     absurd (In U (Add U X x) x0); auto with sets.
-    red in |- *; intro H'5; try exact H'5.
+    red; intro H'5; try exact H'5.
     lapply (Add_inv U X x x0); tauto.
   Qed.
 
@@ -183,11 +183,11 @@ Section Finite_sets_facts.
     intros H'6 H'7; apply f_equal.
     apply H'0 with (Y := X0); auto with sets.
     apply Simplify_add with (x := x); auto with sets.
-    pattern x at 2 in |- *; rewrite H'6; auto with sets.
+    pattern x at 2; rewrite H'6; auto with sets.
     intros H'6 H'7.
     absurd (Add U X x = Add U X0 x0); auto with sets.
     clear H'0 H' H'3 n H'5 H'4 H'2 H'1 c2.
-    red in |- *; intro H'.
+    red; intro H'.
     lapply (Extension U (Add U X x) (Add U X0 x0)); auto with sets.
     clear H'.
     intro H'; red in H'.
@@ -254,7 +254,7 @@ Section Finite_sets_facts.
     apply H'0 with (Y := X0); auto with sets arith.
     apply sincl_add_x with (x := x0).
     rewrite <- H'6; auto with sets arith.
-    pattern x0 at 1 in |- *; rewrite <- H'6; trivial with sets arith.
+    pattern x0 at 1; rewrite <- H'6; trivial with sets arith.
     intros H'6 H'7; red in H'5.
     elim H'5; intros H'8 H'9; try exact H'8; clear H'5.
     red in H'8.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 24facb6f6..440e636cb 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -55,7 +55,7 @@ Section Image.
   Proof.
     intros X x f.
     apply Extensionality_Ensembles.
-    split; red in |- *; intros x0 H'.
+    split; red; intros x0 H'.
     elim H'; intros.
     rewrite H0.
     elim Add_inv with U X x x1; auto using Im_def with sets.
@@ -72,7 +72,7 @@ Section Image.
     intro f; try assumption.
     apply Extensionality_Ensembles.
     split; auto with sets.
-    red in |- *.
+    red.
     intros x H'; elim H'.
     intros x0 H'0; elim H'0; auto with sets.
   Qed.
@@ -102,7 +102,7 @@ Section Image.
     forall f:U -> V,
       ~ injective f ->  exists x : _, (exists y : _, f x = f y /\ x <> y).
   Proof.
-    unfold injective in |- *; intros f H.
+    unfold injective; intros f H.
     cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)).
     2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y);
       trivial with sets.
@@ -153,7 +153,7 @@ Section Image.
     apply cardinal_unicity with V (Add _ (Im A f) (f x)); trivial with sets.
     apply card_add; auto with sets.
     rewrite <- H1; trivial with sets.
-    red in |- *; intro; apply H'2.
+    red; intro; apply H'2.
     apply In_Image_elim with f; trivial with sets.
   Qed.
 
@@ -180,7 +180,7 @@ Section Image.
       cardinal U A n ->
       forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.
   Proof.
-    unfold not in |- *; intros A f n CAn n' CIfn' ltn'n I.
+    unfold not; intros A f n CAn n' CIfn' ltn'n I.
     cut (n' = n).
     intro E; generalize ltn'n; rewrite E; exact (lt_irrefl n).
     apply injective_preserves_cardinal with (A := A) (f := f) (n := n);
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index a21fe880c..f2862e14e 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -56,7 +56,7 @@ Section Infinite_sets.
     intros A X H' H'0.
     elim H'0; intros H'1 H'2.
     apply Strict_super_set_contains_new_element; auto with sets.
-    red in |- *; intro H'3; apply H'.
+    red; intro H'3; apply H'.
     rewrite <- H'3; auto with sets.
   Qed.
 
@@ -76,7 +76,7 @@ Section Infinite_sets.
     split.
     apply card_add; auto with sets.
     cut (In U A x).
-    intro H'4; red in |- *; auto with sets.
+    intro H'4; red; auto with sets.
     intros x0 H'5; elim H'5; auto with sets.
     intros x1 H'6; elim H'6; auto with sets.
     elim H'3; auto with sets.
@@ -91,7 +91,7 @@ Section Infinite_sets.
     split.
     apply card_add; auto with sets.
     elim H'2; auto with sets.
-    red in |- *.
+    red.
     intros x2 H'9; elim H'9; auto with sets.
     intros x3 H'10; elim H'10; auto with sets.
     elim H'2; auto with sets.
@@ -167,11 +167,11 @@ Section Infinite_sets.
     apply ex_intro with (x := Add U x0 x1).
     split; [ split; [ try assumption | idtac ] | idtac ].
     apply card_add; auto with sets.
-    red in |- *; intro H'9; try exact H'9.
+    red; intro H'9; try exact H'9.
     apply H'1.
     elim H'4; intros H'10 H'11; rewrite <- H'11; clear H'4; auto with sets.
     elim H'4; intros H'9 H'10; try exact H'9; clear H'4; auto with sets.
-    red in |- *; auto with sets.
+    red; auto with sets.
     intros x2 H'4; elim H'4; auto with sets.
     intros x3 H'11; elim H'11; auto with sets.
     elim H'4; intros H'9 H'10; rewrite <- H'10; clear H'4; auto with sets.
@@ -235,7 +235,7 @@ Section Infinite_sets.
   Proof.
     intros A f H' H'0 H'1.
     apply NNPP.
-    red in |- *; intro H'2.
+    red; intro H'2.
     elim (Pigeonhole_bis A f); auto with sets.
   Qed.
 
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 2c94a2e16..5ba7856eb 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -49,17 +49,17 @@ Section Integers_sect.
 
   Lemma le_reflexive : Reflexive nat le.
   Proof.
-    red in |- *; auto with arith.
+    red; auto with arith.
   Qed.
 
   Lemma le_antisym : Antisymmetric nat le.
   Proof.
-    red in |- *; intros x y H H'; rewrite (le_antisym x y); auto.
+    red; intros x y H H'; rewrite (le_antisym x y); auto.
   Qed.
 
   Lemma le_trans : Transitive nat le.
   Proof.
-    red in |- *; intros; apply le_trans with y; auto.
+    red; intros; apply le_trans with y; auto.
   Qed.
 
   Lemma le_Order : Order nat le.
@@ -83,7 +83,7 @@ Section Integers_sect.
   Lemma le_total_order : Totally_ordered nat nat_po Integers.
   Proof.
     apply Totally_ordered_definition.
-    simpl in |- *.
+    simpl.
     intros H' x y H'0.
     elim le_or_lt with (n := x) (m := y).
     intro H'1; left; auto with sets arith.
@@ -103,7 +103,7 @@ Section Integers_sect.
     intros A H'0 H'1 x H'2; try assumption.
     elim H'1; intros x0 H'3; clear H'1.
     elim le_total_order.
-    simpl in |- *.
+    simpl.
     intro H'1; try assumption.
     lapply H'1; [ intro H'4; idtac | try assumption ]; auto with sets arith.
     generalize (H'4 x0 x).
@@ -114,28 +114,28 @@ Section Integers_sect.
 	[ intro H'5; try exact H'5; clear H'4 H'1 | intro H'5; clear H'4 H'1 ]
 	| clear H'1 ].
     exists x.
-    apply Upper_Bound_definition. simpl in |- *. apply triv_nat.
+    apply Upper_Bound_definition. simpl. apply triv_nat.
     intros y H'1; elim H'1.
     generalize le_trans.
     intro H'4; red in H'4.
     intros x1 H'6; try assumption.
-    apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial.
+    apply H'4 with (y := x0). elim H'3; simpl; auto with sets arith. trivial.
     intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial.
     exists x0.
     apply Upper_Bound_definition.
       unfold nat_po. simpl. apply triv_nat.
     intros y H'1; elim H'1.
     intros x1 H'4; try assumption.
-    elim H'3; simpl in |- *; auto with sets arith.
+    elim H'3; simpl; auto with sets arith.
     intros x1 H'4; elim H'4; auto with sets arith.
-    red in |- *.
+    red.
     intros x1 H'1; elim H'1; apply triv_nat.
   Qed.
 
   Lemma Integers_has_no_ub :
     ~ (exists m : nat, Upper_Bound nat nat_po Integers m).
   Proof.
-    red in |- *; intro H'; elim H'.
+    red; intro H'; elim H'.
     intros x H'0.
     elim H'0; intros H'1 H'2.
     cut (In nat Integers (S x)).
@@ -150,7 +150,7 @@ Section Integers_sect.
   Lemma Integers_infinite : ~ Finite nat Integers.
   Proof.
     generalize Integers_has_no_ub.
-    intro H'; red in |- *; intro H'0; try exact H'0.
+    intro H'; red; intro H'0; try exact H'0.
     apply H'.
     apply Finite_subset_has_lub; auto with sets arith.
   Qed.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 5f21335fd..4159d3877 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -42,14 +42,14 @@ Section multiset_defs.
 
   Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.
   Proof.
-    unfold meq in |- *.
+    unfold meq.
     destruct x; destruct y; destruct z.
     intros; rewrite H; auto.
   Qed.
 
   Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.
   Proof.
-    unfold meq in |- *.
+    unfold meq.
     destruct x; destruct y; auto.
   Qed.
 
@@ -59,12 +59,12 @@ Section multiset_defs.
 
   Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).
   Proof.
-    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+    unfold meq; unfold munion; simpl; auto.
   Qed.
 
   Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).
   Proof.
-    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.
+    unfold meq; unfold munion; simpl; auto.
   Qed.
 
 
@@ -72,21 +72,21 @@ Section multiset_defs.
 
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
-    unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.
+    unfold meq; unfold multiplicity; unfold munion.
     destruct x; destruct y; auto with arith.
   Qed.
 
   Lemma munion_ass :
     forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).
   Proof.
-    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    unfold meq; unfold munion; unfold multiplicity.
     destruct x; destruct y; destruct z; auto with arith.
   Qed.
 
   Lemma meq_left :
     forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).
   Proof.
-    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    unfold meq; unfold munion; unfold multiplicity.
     destruct x; destruct y; destruct z.
     intros; elim H; auto with arith.
   Qed.
@@ -94,7 +94,7 @@ Section multiset_defs.
   Lemma meq_right :
     forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).
   Proof.
-    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.
+    unfold meq; unfold munion; unfold multiplicity.
     destruct x; destruct y; destruct z.
     intros; elim H; auto.
   Qed.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index a319b9832..bb1cf7083 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -63,13 +63,13 @@ Section Partial_order_facts.
     forall x y z:U,
       Strict_Rel_of U D x y -> Rel_of U D y z -> Strict_Rel_of U D x z.
   Proof.
-    unfold Strict_Rel_of at 1 in |- *.
-    red in |- *.
-    elim D; simpl in |- *.
+    unfold Strict_Rel_of at 1.
+    red.
+    elim D; simpl.
     intros C R H' H'0; elim H'0.
     intros H'1 H'2 H'3 x y z H'4 H'5; split.
     apply H'2 with (y := y); tauto.
-    red in |- *; intro H'6.
+    red; intro H'6.
     elim H'4; intros H'7 H'8; apply H'8; clear H'4.
     apply H'3; auto.
     rewrite H'6; tauto.
@@ -79,20 +79,20 @@ Section Partial_order_facts.
     forall x y z:U,
       Rel_of U D x y -> Strict_Rel_of U D y z -> Strict_Rel_of U D x z.
   Proof.
-    unfold Strict_Rel_of at 1 in |- *.
-    red in |- *.
-    elim D; simpl in |- *.
+    unfold Strict_Rel_of at 1.
+    red.
+    elim D; simpl.
     intros C R H' H'0; elim H'0.
     intros H'1 H'2 H'3 x y z H'4 H'5; split.
     apply H'2 with (y := y); tauto.
-    red in |- *; intro H'6.
+    red; intro H'6.
     elim H'5; intros H'7 H'8; apply H'8; clear H'5.
     apply H'3; auto.
     rewrite <- H'6; auto.
   Qed.
 
   Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
-    red in |- *.
+    red.
     intros x y z H' H'0.
     apply Strict_Rel_Transitive_with_Rel with (y := y);
       [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index f8b24e747..f3b7c4deb 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -39,7 +39,7 @@ Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
 Hint Resolve Definition_of_Power_set.
 
 Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
-intro X; red in |- *.
+intro X; red.
 intros x H'; elim H'.
 Qed.
 Hint Resolve Empty_set_minimal.
@@ -79,7 +79,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion :
    Strict_Included U x y -> Included U y z -> Strict_Included U x z.
 intros x y z H' H'0; try assumption.
 elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
 intros H'1 H'2; try assumption.
 apply H'1.
 apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets.
@@ -90,7 +90,7 @@ Lemma Strict_inclusion_is_transitive_with_inclusion_left :
    Included U x y -> Strict_Included U y z -> Strict_Included U x z.
 intros x y z H' H'0; try assumption.
 elim Strict_Rel_is_Strict_Included.
-unfold contains in |- *.
+unfold contains.
 intros H'1 H'2; try assumption.
 apply H'1.
 apply Strict_Rel_Transitive_with_Rel_left with (y := y); auto with sets.
@@ -105,14 +105,14 @@ Qed.
 
 Theorem Empty_set_is_Bottom :
  forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
-intro A; apply Bottom_definition; simpl in |- *; auto with sets.
+intro A; apply Bottom_definition; simpl; auto with sets.
 Qed.
 Hint Resolve Empty_set_is_Bottom.
 
 Theorem Union_minimal :
  forall a b X:Ensemble U,
    Included U a X -> Included U b X -> Included U (Union U a b) X.
-intros a b X H' H'0; red in |- *.
+intros a b X H' H'0; red.
 intros x H'1; elim H'1; auto with sets.
 Qed.
 Hint Resolve Union_minimal.
@@ -133,13 +133,13 @@ Qed.
 
 Theorem Intersection_decreases_l :
  forall a b:Ensemble U, Included U (Intersection U a b) a.
-intros a b; red in |- *.
+intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
 
 Theorem Intersection_decreases_r :
  forall a b:Ensemble U, Included U (Intersection U a b) b.
-intros a b; red in |- *.
+intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
 Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
@@ -151,10 +151,10 @@ Theorem Union_is_Lub :
    Included U b A ->
    Lub (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b) (Union U a b).
 intros A a b H' H'0.
-apply Lub_definition; simpl in |- *.
-apply Upper_Bound_definition; simpl in |- *; auto with sets.
+apply Lub_definition; simpl.
+apply Upper_Bound_definition; simpl; auto with sets.
 intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 Theorem Intersection_is_Glb :
@@ -164,13 +164,13 @@ Theorem Intersection_is_Glb :
    Glb (Ensemble U) (Power_set_PO A) (Couple (Ensemble U) a b)
      (Intersection U a b).
 intros A a b H' H'0.
-apply Glb_definition; simpl in |- *.
-apply Lower_Bound_definition; simpl in |- *; auto with sets.
+apply Glb_definition; simpl.
+apply Lower_Bound_definition; simpl; auto with sets.
 apply Definition_of_Power_set.
 generalize Inclusion_is_transitive; intro IT; red in IT; apply IT with a;
  auto with sets.
 intros y H'1; elim H'1; auto with sets.
-intros y H'1; elim H'1; simpl in |- *; auto with sets.
+intros y H'1; elim H'1; simpl; auto with sets.
 Qed.
 
 End The_power_set_partial_order.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 09fc20948..a7601aaaf 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -44,13 +44,13 @@ Section Sets_as_an_algebra.
       ~ In U A x ->
       Strict_Included U (Add U A x) (Add U B x) -> Strict_Included U A B.
   Proof.
-    intros A B x H' H'0; red in |- *.
+    intros A B x H' H'0; red.
     lapply (Strict_Included_inv U (Add U A x) (Add U B x)); auto with sets.
     clear H'0; intro H'0; split.
     apply incl_add_x with (x := x); tauto.
     elim H'0; intros H'1 H'2; elim H'2; clear H'0 H'2.
     intros x0 H'0.
-    red in |- *; intro H'2.
+    red; intro H'2.
     elim H'0; clear H'0.
     rewrite <- H'2; auto with sets.
   Qed.
@@ -58,7 +58,7 @@ Section Sets_as_an_algebra.
   Lemma incl_soustr_in :
     forall (X:Ensemble U) (x:U), In U X x -> Included U (Subtract U X x) X.
   Proof.
-    intros X x H'; red in |- *.
+    intros X x H'; red.
     intros x0 H'0; elim H'0; auto with sets.
   Qed.
 
@@ -66,7 +66,7 @@ Section Sets_as_an_algebra.
     forall (X Y:Ensemble U) (x:U),
       Included U X Y -> Included U (Subtract U X x) (Subtract U Y x).
   Proof.
-    intros X Y x H'; red in |- *.
+    intros X Y x H'; red.
     intros x0 H'0; elim H'0.
     intros H'1 H'2.
     apply Subtract_intro; auto with sets.
@@ -75,7 +75,7 @@ Section Sets_as_an_algebra.
   Lemma incl_soustr_add_l :
     forall (X:Ensemble U) (x:U), Included U (Subtract U (Add U X x) x) X.
   Proof.
-    intros X x; red in |- *.
+    intros X x; red.
     intros x0 H'; elim H'; auto with sets.
     intro H'0; elim H'0; auto with sets.
     intros t H'1 H'2; elim H'2; auto with sets.
@@ -85,10 +85,10 @@ Section Sets_as_an_algebra.
     forall (X:Ensemble U) (x:U),
       ~ In U X x -> Included U X (Subtract U (Add U X x) x).
   Proof.
-    intros X x H'; red in |- *.
+    intros X x H'; red.
     intros x0 H'0; try assumption.
     apply Subtract_intro; auto with sets.
-    red in |- *; intro H'1; apply H'; rewrite H'1; auto with sets.
+    red; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
   Hint Resolve incl_soustr_add_r: sets v62.
 
@@ -96,7 +96,7 @@ Section Sets_as_an_algebra.
     forall (X:Ensemble U) (x:U),
       In U X x -> Included U X (Add U (Subtract U X x) x).
   Proof.
-    intros X x H'; red in |- *.
+    intros X x H'; red.
     intros x0 H'0; try assumption.
     elim (classic (x = x0)); intro K; auto with sets.
     elim K; auto with sets.
@@ -106,7 +106,7 @@ Section Sets_as_an_algebra.
     forall (X:Ensemble U) (x:U),
       In U X x -> Included U (Add U (Subtract U X x) x) X.
   Proof.
-    intros X x H'; red in |- *.
+    intros X x H'; red.
     intros x0 H'0; elim H'0; auto with sets.
     intros y H'1; elim H'1; auto with sets.
     intros t H'1; try assumption.
@@ -118,7 +118,7 @@ Section Sets_as_an_algebra.
       x <> y -> Subtract U (Add U X x) y = Add U (Subtract U X y) x.
   Proof.
     intros X x y H'; apply Extensionality_Ensembles.
-    split; red in |- *.
+    split; red.
     intros x0 H'0; elim H'0; auto with sets.
     intro H'1; elim H'1.
     intros u H'2 H'3; try assumption.
@@ -146,7 +146,7 @@ Section Sets_as_an_algebra.
     apply H'4 with (y := Y); auto using add_soustr_2 with sets.
     red in H'0.
     elim H'0; intros H'1 H'2; try exact H'1; clear H'0. (* PB *)
-    red in |- *; intro H'0; apply H'2.
+    red; intro H'0; apply H'2.
     rewrite H'0; auto 8 using add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
   Qed.
 
@@ -177,7 +177,7 @@ Section Sets_as_an_algebra.
     exists (Subtract U X x).
     split; auto using incl_soustr_in, add_soustr_xy, add_soustr_1, add_soustr_2 with sets.
     red in H'0.
-    red in |- *.
+    red.
     intros x0 H'2; try assumption.
     lapply (Subtract_inv U X x x0); auto with sets.
     intro H'3; elim H'3; intros K K'; clear H'3.
@@ -189,7 +189,7 @@ Section Sets_as_an_algebra.
     elim K'; auto with sets.
     intro H'1; left; try assumption.
     red in H'0.
-    red in |- *.
+    red.
     intros x0 H'2; try assumption.
     lapply (H'0 x0); auto with sets.
     intro H'3; try assumption.
@@ -207,7 +207,7 @@ Section Sets_as_an_algebra.
       (forall z:Ensemble U, Included U x z -> Included U z y -> x = z \/ z = y).
   Proof.
     intros A x y H'; elim H'.
-    unfold Strict_Rel_of in |- *; simpl in |- *.
+    unfold Strict_Rel_of; simpl.
     intros H'0 H'1; split; [ auto with sets | idtac ].
     intros z H'2 H'3; try assumption.
     elim (classic (x = z)); auto with sets.
@@ -227,11 +227,11 @@ Section Sets_as_an_algebra.
   Proof.
     intros A a H' x H'0 H'1; try assumption.
     apply setcover_intro; auto with sets.
-    red in |- *.
-    split; [ idtac | red in |- *; intro H'2; try exact H'2 ]; auto with sets.
+    red.
+    split; [ idtac | red; intro H'2; try exact H'2 ]; auto with sets.
     apply H'1.
     rewrite H'2; auto with sets.
-    red in |- *; intro H'2; elim H'2; clear H'2.
+    red; intro H'2; elim H'2; clear H'2.
     intros z H'2; elim H'2; intros H'3 H'4; try exact H'3; clear H'2.
     lapply (Strict_Included_inv U a z); auto with sets; clear H'3.
     intro H'2; elim H'2; intros H'3 H'5; elim H'5; clear H'2 H'5.
@@ -249,7 +249,7 @@ Section Sets_as_an_algebra.
     red in K.
     elim K; intros H'11 H'12; apply H'12; clear K; auto with sets.
     rewrite H'15.
-    red in |- *.
+    red.
     intros x1 H'10; elim H'10; auto with sets.
     intros x2 H'11; elim H'11; auto with sets.
   Qed.
@@ -275,11 +275,11 @@ Section Sets_as_an_algebra.
     elim (H'7 (Add U a x)); auto with sets.
     intro H'1.
     absurd (a = Add U a x); auto with sets.
-    red in |- *; intro H'8; try exact H'8.
+    red; intro H'8; try exact H'8.
     apply H'3.
     rewrite H'8; auto with sets.
     auto with sets.
-    red in |- *.
+    red.
     intros x0 H'1; elim H'1; auto with sets.
     intros x1 H'8; elim H'8; auto with sets.
     split; [ idtac | try assumption ].
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index f756f9854..14a2d25cc 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -42,7 +42,7 @@ Section Sets_as_an_algebra.
 
   Theorem Empty_set_zero' : forall x:U, Add U (Empty_set U) x = Singleton U x.
   Proof.
-    unfold Add at 1 in |- *; auto using Empty_set_zero with sets.
+    unfold Add at 1; auto using Empty_set_zero with sets.
   Qed.
 
   Lemma less_than_empty :
@@ -76,7 +76,7 @@ Section Sets_as_an_algebra.
   Theorem Couple_as_union :
     forall x y:U, Union U (Singleton U x) (Singleton U y) = Couple U x y.
   Proof.
-    intros x y; apply Extensionality_Ensembles; split; red in |- *.
+    intros x y; apply Extensionality_Ensembles; split; red.
     intros x0 H'; elim H'; (intros x1 H'0; elim H'0; auto with sets).
     intros x0 H'; elim H'; auto with sets.
   Qed.
@@ -86,7 +86,7 @@ Section Sets_as_an_algebra.
       Union U (Union U (Singleton U x) (Singleton U y)) (Singleton U z) =
       Triple U x y z.
   Proof.
-    intros x y z; apply Extensionality_Ensembles; split; red in |- *.
+    intros x y z; apply Extensionality_Ensembles; split; red.
     intros x0 H'; elim H'.
     intros x1 H'0; elim H'0; (intros x2 H'1; elim H'1; auto with sets).
     intros x1 H'0; elim H'0; auto with sets.
@@ -114,7 +114,7 @@ Section Sets_as_an_algebra.
   Proof.
     intros A B.
     apply Extensionality_Ensembles.
-    split; red in |- *; intros x H'; elim H'; auto with sets.
+    split; red; intros x H'; elim H'; auto with sets.
   Qed.
 
   Theorem Distributivity :
@@ -124,7 +124,7 @@ Section Sets_as_an_algebra.
   Proof.
     intros A B C.
     apply Extensionality_Ensembles.
-    split; red in |- *; intros x H'.
+    split; red; intros x H'.
     elim H'.
     intros x0 H'0 H'1; generalize H'0.
     elim H'1; auto with sets.
@@ -138,7 +138,7 @@ Section Sets_as_an_algebra.
   Proof.
     intros A B C.
     apply Extensionality_Ensembles.
-    split; red in |- *; intros x H'.
+    split; red; intros x H'.
     elim H'; auto with sets.
     intros x0 H'0; elim H'0; auto with sets.
     elim H'.
@@ -151,15 +151,15 @@ Section Sets_as_an_algebra.
   Theorem Union_add :
     forall (A B:Ensemble U) (x:U), Add U (Union U A B) x = Union U A (Add U B x).
   Proof.
-    unfold Add in |- *; auto using Union_associative with sets.
+    unfold Add; auto using Union_associative with sets.
   Qed.
 
   Theorem Non_disjoint_union :
     forall (X:Ensemble U) (x:U), In U X x -> Add U X x = X.
   Proof.
-    intros X x H'; unfold Add in |- *.
-    apply Extensionality_Ensembles; red in |- *.
-    split; red in |- *; auto with sets.
+    intros X x H'; unfold Add.
+    apply Extensionality_Ensembles; red.
+    split; red; auto with sets.
     intros x0 H'0; elim H'0; auto with sets.
     intros t H'1; elim H'1; auto with sets.
   Qed.
@@ -167,12 +167,12 @@ Section Sets_as_an_algebra.
   Theorem Non_disjoint_union' :
     forall (X:Ensemble U) (x:U), ~ In U X x -> Subtract U X x = X.
   Proof.
-    intros X x H'; unfold Subtract in |- *.
+    intros X x H'; unfold Subtract.
     apply Extensionality_Ensembles.
-    split; red in |- *; auto with sets.
+    split; red; auto with sets.
     intros x0 H'0; elim H'0; auto with sets.
     intros x0 H'0; apply Setminus_intro; auto with sets.
-    red in |- *; intro H'1; elim H'1.
+    red; intro H'1; elim H'1.
     lapply (Singleton_inv U x x0); auto with sets.
     intro H'4; apply H'; rewrite H'4; auto with sets.
   Qed.
@@ -186,7 +186,7 @@ Section Sets_as_an_algebra.
     forall (A B:Ensemble U) (x:U),
       Included U A B -> Included U (Add U A x) (Add U B x).
   Proof.
-    intros A B x H'; red in |- *; auto with sets.
+    intros A B x H'; red; auto with sets.
     intros x0 H'0.
     lapply (Add_inv U A x x0); auto with sets.
     intro H'1; elim H'1;
@@ -198,7 +198,7 @@ Section Sets_as_an_algebra.
     forall (A B:Ensemble U) (x:U),
       ~ In U A x -> Included U (Add U A x) (Add U B x) -> Included U A B.
   Proof.
-    unfold Included in |- *.
+    unfold Included.
     intros A B x H' H'0 x0 H'1.
     lapply (H'0 x0); auto with sets.
     intro H'2; lapply (Add_inv U B x x0); auto with sets.
@@ -212,7 +212,7 @@ Section Sets_as_an_algebra.
     forall (A:Ensemble U) (x y:U), Add U (Add U A x) y = Add U (Add U A y) x.
   Proof.
     intros A x y.
-    unfold Add in |- *.
+    unfold Add.
     rewrite (Union_associative A (Singleton U x) (Singleton U y)).
     rewrite (Union_commutative (Singleton U x) (Singleton U y)).
     rewrite <- (Union_associative A (Singleton U y) (Singleton U x));
@@ -234,7 +234,7 @@ Section Sets_as_an_algebra.
   Proof.
     intros A B x y H'; try assumption.
     rewrite <- (Union_add (Add U A x) B y).
-    unfold Add at 4 in |- *.
+    unfold Add at 4.
     rewrite (Union_commutative A (Singleton U x)).
     rewrite Union_associative.
     rewrite (Union_absorbs A B H').
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 0c8329dd0..efd895e2c 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -33,8 +33,8 @@ Theorem Rsym_imp_notRsym :
  forall (U:Type) (R:Relation U),
    Symmetric U R -> Symmetric U (Complement U R).
 Proof.
-unfold Symmetric, Complement in |- *.
-intros U R H' x y H'0; red in |- *; intro H'1; apply H'0; auto with sets.
+unfold Symmetric, Complement.
+intros U R H' x y H'0; red; intro H'1; apply H'0; auto with sets.
 Qed.
 
 Theorem Equiv_from_preorder :
@@ -44,8 +44,8 @@ Proof.
 intros U R H'; elim H'; intros H'0 H'1.
 apply Definition_of_equivalence.
 red in H'0; auto 10 with sets.
-2: red in |- *; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
-red in H'1; red in |- *; auto 10 with sets.
+2: red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets.
+red in H'1; red; auto 10 with sets.
 intros x y z h; elim h; intros H'3 H'4; clear h.
 intro h; elim h; intros H'5 H'6; clear h.
 split; apply H'1 with y; auto 10 with sets.
@@ -70,7 +70,7 @@ Hint Resolve contains_is_preorder.
 Theorem same_relation_is_equivalence :
  forall U:Type, Equivalence (Relation U) (same_relation U).
 Proof.
-unfold same_relation at 1 in |- *; auto 10 with sets.
+unfold same_relation at 1; auto 10 with sets.
 Qed.
 Hint Resolve same_relation_is_equivalence.
 
@@ -78,14 +78,14 @@ Theorem cong_reflexive_same_relation :
  forall (U:Type) (R R':Relation U),
    same_relation U R R' -> Reflexive U R -> Reflexive U R'.
 Proof.
-unfold same_relation in |- *; intuition.
+unfold same_relation; intuition.
 Qed.
 
 Theorem cong_symmetric_same_relation :
  forall (U:Type) (R R':Relation U),
    same_relation U R R' -> Symmetric U R -> Symmetric U R'.
 Proof.
-  compute in |- *; intros; elim H; intros; clear H;
+  compute; intros; elim H; intros; clear H;
    apply (H3 y x (H0 x y (H2 x y H1))).
 (*Intuition.*)
 Qed.
@@ -94,7 +94,7 @@ Theorem cong_antisymmetric_same_relation :
  forall (U:Type) (R R':Relation U),
    same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
 Proof.
-  compute in |- *; intros; elim H; intros; clear H;
+  compute; intros; elim H; intros; clear H;
    apply (H0 x y (H3 x y H1) (H3 y x H2)).
 (*Intuition.*)
 Qed.
@@ -103,7 +103,7 @@ Theorem cong_transitive_same_relation :
  forall (U:Type) (R R':Relation U),
    same_relation U R R' -> Transitive U R -> Transitive U R'.
 Proof.
-intros U R R' H' H'0; red in |- *.
+intros U R R' H' H'0; red.
 elim H'.
 intros H'1 H'2 x y z H'3 H'4; apply H'2.
 apply H'0 with y; auto with sets.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 89b98c1f5..bc5960ebe 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -43,13 +43,13 @@ Qed.
 Theorem Rstar_contains_R :
  forall (U:Type) (R:Relation U), contains U (Rstar U R) R.
 Proof.
-intros U R; red in |- *; intros x y H'; apply Rstar_n with y; auto with sets.
+intros U R; red; intros x y H'; apply Rstar_n with y; auto with sets.
 Qed.
 
 Theorem Rstar_contains_Rplus :
  forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).
 Proof.
-intros U R; red in |- *.
+intros U R; red.
 intros x y H'; elim H'.
 generalize Rstar_contains_R; intro T; red in T; auto with sets.
 intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto with sets.
@@ -58,7 +58,7 @@ Qed.
 Theorem Rstar_transitive :
  forall (U:Type) (R:Relation U), Transitive U (Rstar U R).
 Proof.
-intros U R; red in |- *.
+intros U R; red.
 intros x y z H'; elim H'; auto with sets.
 intros x0 y0 z0 H'0 H'1 H'2 H'3; apply Rstar_n with y0; auto with sets.
 Qed.
@@ -75,7 +75,7 @@ Theorem Rstar_equiv_Rstar1 :
  forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).
 Proof.
 generalize Rstar_contains_R; intro T; red in T.
-intros U R; unfold same_relation, contains in |- *.
+intros U R; unfold same_relation, contains.
 split; intros x y H'; elim H'; auto with sets.
 generalize Rstar_transitive; intro T1; red in T1.
 intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets.
@@ -85,7 +85,7 @@ Qed.
 Theorem Rsym_imp_Rstarsym :
  forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).
 Proof.
-intros U R H'; red in |- *.
+intros U R H'; red.
 intros x y H'0; elim H'0; auto with sets.
 intros x0 y0 z H'1 H'2 H'3.
 generalize Rstar_transitive; intro T1; red in T1.
@@ -97,7 +97,7 @@ Theorem Sstar_contains_Rstar :
  forall (U:Type) (R S:Relation U),
    contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).
 Proof.
-unfold contains in |- *.
+unfold contains.
 intros U R S H' x y H'0; elim H'0; auto with sets.
 generalize Rstar_transitive; intro T1; red in T1.
 intros x0 y0 z H'1 H'2 H'3; apply T1 with y0; auto with sets.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 8ac6e7fb4..455ad5843 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -33,7 +33,7 @@ Require Export Relations_3.
 Theorem Rstar_imp_coherent :
  forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y.
 Proof.
-intros U R x y H'; red in |- *.
+intros U R x y H'; red.
 exists y; auto with sets.
 Qed.
 Hint Resolve Rstar_imp_coherent.
@@ -41,8 +41,8 @@ Hint Resolve Rstar_imp_coherent.
 Theorem coherent_symmetric :
  forall (U:Type) (R:Relation U), Symmetric U (coherent U R).
 Proof.
-unfold coherent at 1 in |- *.
-intros U R; red in |- *.
+unfold coherent at 1.
+intros U R; red.
 intros x y H'; elim H'.
 intros z H'0; exists z; tauto.
 Qed.
@@ -50,9 +50,9 @@ Qed.
 Theorem Strong_confluence :
  forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
 Proof.
-intros U R H'; red in |- *.
-intro x; red in |- *; intros a b H'0.
-unfold coherent at 1 in |- *.
+intros U R H'; red.
+intro x; red; intros a b H'0.
+unfold coherent at 1.
 generalize b; clear b.
 elim H'0; clear H'0.
 intros x0 b H'1; exists b; auto with sets.
@@ -75,9 +75,9 @@ Qed.
 Theorem Strong_confluence_direct :
  forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.
 Proof.
-intros U R H'; red in |- *.
-intro x; red in |- *; intros a b H'0.
-unfold coherent at 1 in |- *.
+intros U R H'; red.
+intro x; red; intros a b H'0.
+unfold coherent at 1.
 generalize b; clear b.
 elim H'0; clear H'0.
 intros x0 b H'1; exists b; auto with sets.
@@ -111,7 +111,7 @@ Theorem Noetherian_contains_Noetherian :
  forall (U:Type) (R R':Relation U),
    Noetherian U R -> contains U R R' -> Noetherian U R'.
 Proof.
-unfold Noetherian at 2 in |- *.
+unfold Noetherian at 2.
 intros U R R' H' H'0 x.
 elim (H' x); auto with sets.
 Qed.
@@ -120,8 +120,8 @@ Theorem Newman :
  forall (U:Type) (R:Relation U),
    Noetherian U R -> Locally_confluent U R -> Confluent U R.
 Proof.
-intros U R H' H'0; red in |- *; intro x.
-elim (H' x); unfold confluent in |- *.
+intros U R H' H'0; red; intro x.
+elim (H' x); unfold confluent.
 intros x0 H'1 H'2 y z H'3 H'4.
 generalize (Rstar_cases U R x0 y); intro h; lapply h;
  [ intro h0; elim h0;
@@ -163,7 +163,7 @@ generalize (H'2 v); intro h; lapply h;
        | clear h h0 ]
     | clear h h0 ]
  | clear h ]; auto with sets.
-red in |- *; (exists z1; split); auto with sets.
+red; (exists z1; split); auto with sets.
 apply T with y1; auto with sets.
 apply T with t; auto with sets.
 Qed.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index bf1aaf8db..ca4519ee4 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -51,37 +51,37 @@ Hint Unfold seq.
 
 Lemma leb_refl : forall b:bool, leb b b.
 Proof.
-destruct b; simpl in |- *; auto.
+destruct b; simpl; auto.
 Qed.
 Hint Resolve leb_refl.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 Proof.
-unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+unfold incl; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
 Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1.
 Proof.
-unfold incl in |- *; intros s1 s2 E a; elim (E a); auto.
+unfold incl; intros s1 s2 E a; elim (E a); auto.
 Qed.
 
 Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
-destruct x; unfold seq in |- *; auto.
+destruct x; unfold seq; auto.
 Qed.
 Hint Resolve seq_refl.
 
 Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
 Proof.
-unfold seq in |- *.
-destruct x; destruct y; destruct z; simpl in |- *; intros.
+unfold seq.
+destruct x; destruct y; destruct z; simpl; intros.
 rewrite H; auto.
 Qed.
 
 Lemma seq_sym : forall x y:uniset, seq x y -> seq y x.
 Proof.
-unfold seq in |- *.
-destruct x; destruct y; simpl in |- *; auto.
+unfold seq.
+destruct x; destruct y; simpl; auto.
 Qed.
 
 (** uniset union *)
@@ -90,20 +90,20 @@ Definition union (m1 m2:uniset) :=
 
 Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
 Proof.
-unfold seq in |- *; unfold union in |- *; simpl in |- *; auto.
+unfold seq; unfold union; simpl; auto.
 Qed.
 Hint Resolve union_empty_left.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
 Proof.
-unfold seq in |- *; unfold union in |- *; simpl in |- *.
+unfold seq; unfold union; simpl.
 intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
 Hint Resolve union_empty_right.
 
 Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
 Proof.
-unfold seq in |- *; unfold charac in |- *; unfold union in |- *.
+unfold seq; unfold charac; unfold union.
 destruct x; destruct y; auto with bool.
 Qed.
 Hint Resolve union_comm.
@@ -111,14 +111,14 @@ Hint Resolve union_comm.
 Lemma union_ass :
  forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z; auto with bool.
 Qed.
 Hint Resolve union_ass.
 
 Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
@@ -126,7 +126,7 @@ Hint Resolve seq_left.
 
 Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
 Proof.
-unfold seq in |- *; unfold union in |- *; unfold charac in |- *.
+unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.