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

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.