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

1 files changed, 9 insertions, 9 deletions

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.