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

diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7a6f38fc2..85ecf97e2 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -49,21 +49,21 @@ Qed.
 Lemma tl_nth_tl :
  forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).
 Proof.
-  simple induction n; simpl in |- *; auto.
+  simple induction n; simpl; auto.
 Qed.
 Hint Resolve tl_nth_tl: datatypes v62.
 
 Lemma Str_nth_tl_plus :
  forall (n m:nat) (s:Stream),
    Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.
-simple induction n; simpl in |- *; intros; auto with datatypes.
+simple induction n; simpl; intros; auto with datatypes.
 rewrite <- H.
 rewrite tl_nth_tl; trivial with datatypes.
 Qed.
 
 Lemma Str_nth_plus :
  forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.
-intros; unfold Str_nth in |- *; rewrite Str_nth_tl_plus;
+intros; unfold Str_nth; rewrite Str_nth_tl_plus;
  trivial with datatypes.
 Qed.
 
@@ -89,7 +89,7 @@ Qed.
 
 Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.
 coinduction Eq_sym.
-case H; intros; symmetry  in |- *; assumption.
+case H; intros; symmetry ; assumption.
 case H; intros; assumption.
 Qed.
 
@@ -110,10 +110,10 @@ Qed.
 
 Theorem eqst_ntheq :
  forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.
-unfold Str_nth in |- *; simple induction n.
+unfold Str_nth; simple induction n.
 intros s1 s2 H; case H; trivial with datatypes.
 intros m hypind.
-simpl in |- *.
+simpl.
 intros s1 s2 H.
 apply hypind.
 case H; trivial with datatypes.