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

2 files changed, 44 insertions, 44 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index d67baf57f..26bfa6d35 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -85,15 +85,15 @@ Section first_definitions.
   Lemma set_In_dec : forall (a:A) (x:set), {set_In a x} + {~ set_In a x}.
 
   Proof.
-    unfold set_In in |- *.
+    unfold set_In.
     (*** Realizer set_mem. Program_all. ***)
     simple induction x.
     auto.
     intros a0 x0 Ha0. case (Aeq_dec a a0); intro eq.
-    rewrite eq; simpl in |- *; auto with datatypes.
+    rewrite eq; simpl; auto with datatypes.
     elim Ha0.
     auto with datatypes.
-    right; simpl in |- *; unfold not in |- *; intros [Hc1| Hc2];
+    right; simpl; unfold not; intros [Hc1| Hc2];
      auto with datatypes.
   Qed.
 
@@ -102,7 +102,7 @@ Section first_definitions.
      (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
 
   Proof.
-    simple induction x; simpl in |- *; intros.
+    simple induction x; simpl; intros.
     assumption.
     elim (Aeq_dec a a0); auto with datatypes.
   Qed.
@@ -113,11 +113,11 @@ Section first_definitions.
      (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
 
   Proof.
-    simple induction x; simpl in |- *; intros.
-    apply H0; red in |- *; trivial.
+    simple induction x; simpl; intros.
+    apply H0; red; trivial.
     case (Aeq_dec a a0); auto with datatypes.
     intro; apply H; intros; auto.
-    apply H1; red in |- *; intro.
+    apply H1; red; intro.
     case H3; auto.
   Qed.
 
@@ -125,7 +125,7 @@ Section first_definitions.
   Lemma set_mem_correct1 :
    forall (a:A) (x:set), set_mem a x = true -> set_In a x.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     discriminate.
     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
   Qed.
@@ -133,7 +133,7 @@ Section first_definitions.
   Lemma set_mem_correct2 :
    forall (a:A) (x:set), set_In a x -> set_mem a x = true.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     intro Ha; elim Ha.
     intros a0 l; elim (Aeq_dec a a0); auto with datatypes.
     intros H1 H2 [H3| H4].
@@ -144,17 +144,17 @@ Section first_definitions.
   Lemma set_mem_complete1 :
    forall (a:A) (x:set), set_mem a x = false -> ~ set_In a x.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
     intros; discriminate H0.
-    unfold not in |- *; intros; elim H1; auto with datatypes.
+    unfold not; intros; elim H1; auto with datatypes.
   Qed.
 
   Lemma set_mem_complete2 :
    forall (a:A) (x:set), ~ set_In a x -> set_mem a x = false.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     tauto.
     intros a0 l; elim (Aeq_dec a a0).
     intros; elim H0; auto with datatypes.
@@ -165,7 +165,7 @@ Section first_definitions.
    forall (a b:A) (x:set), set_In a x -> set_In a (set_add b x).
 
   Proof.
-    unfold set_In in |- *; simple induction x; simpl in |- *.
+    unfold set_In; simple induction x; simpl.
     auto with datatypes.
     intros a0 l H [Ha0a| Hal].
     elim (Aeq_dec b a0); left; assumption.
@@ -176,11 +176,11 @@ Section first_definitions.
    forall (a b:A) (x:set), a = b -> set_In a (set_add b x).
 
   Proof.
-    unfold set_In in |- *; simple induction x; simpl in |- *.
+    unfold set_In; simple induction x; simpl.
     auto with datatypes.
     intros a0 l H Hab.
     elim (Aeq_dec b a0);
-     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl in |- *;
+     [ rewrite Hab; intro Hba0; rewrite Hba0; simpl;
         auto with datatypes
      | auto with datatypes ].
   Qed.
@@ -198,13 +198,13 @@ Section first_definitions.
    forall (a b:A) (x:set), set_In a (set_add b x) -> a = b \/ set_In a x.
 
   Proof.
-    unfold set_In in |- *.
+    unfold set_In.
     simple induction x.
-    simpl in |- *; intros [H1| H2]; auto with datatypes.
-    simpl in |- *; do 3 intro.
+    simpl; intros [H1| H2]; auto with datatypes.
+    simpl; do 3 intro.
     elim (Aeq_dec b a0).
-    simpl in |- *; tauto.
-    simpl in |- *; intros; elim H0.
+    simpl; tauto.
+    simpl; intros; elim H0.
     trivial with datatypes.
     tauto.
     tauto.
@@ -220,7 +220,7 @@ Section first_definitions.
 
   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
   Proof.
-    simple induction x; simpl in |- *.
+    simple induction x; simpl.
     discriminate.
     intros; elim (Aeq_dec a a0); intros; discriminate.
   Qed.
@@ -229,13 +229,13 @@ Section first_definitions.
   Lemma set_union_intro1 :
    forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
   Proof.
-    simple induction y; simpl in |- *; auto with datatypes.
+    simple induction y; simpl; auto with datatypes.
   Qed.
 
   Lemma set_union_intro2 :
    forall (a:A) (x y:set), set_In a y -> set_In a (set_union x y).
   Proof.
-    simple induction y; simpl in |- *.
+    simple induction y; simpl.
     tauto.
     intros; elim H0; auto with datatypes.
   Qed.
@@ -253,7 +253,7 @@ Section first_definitions.
    forall (a:A) (x y:set),
      set_In a (set_union x y) -> set_In a x \/ set_In a y.
   Proof.
-    simple induction y; simpl in |- *.
+    simple induction y; simpl.
     auto with datatypes.
     intros.
     generalize (set_add_elim _ _ _ H0).
@@ -280,11 +280,11 @@ Section first_definitions.
   Proof.
     simple induction x.
     auto with datatypes.
-    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hy.
-    simpl in |- *; rewrite Ha0a.
+    simpl; intros a0 l Hrec y [Ha0a| Hal] Hy.
+    simpl; rewrite Ha0a.
     generalize (set_mem_correct1 a y).
     generalize (set_mem_complete1 a y).
-    elim (set_mem a y); simpl in |- *; intros.
+    elim (set_mem a y); simpl; intros.
     auto with datatypes.
     absurd (set_In a y); auto with datatypes.
     elim (set_mem a0 y); [ right; auto with datatypes | auto with datatypes ].
@@ -295,9 +295,9 @@ Section first_definitions.
   Proof.
     simple induction x.
     auto with datatypes.
-    simpl in |- *; intros a0 l Hrec y.
+    simpl; intros a0 l Hrec y.
     generalize (set_mem_correct1 a0 y).
-    elim (set_mem a0 y); simpl in |- *; intros.
+    elim (set_mem a0 y); simpl; intros.
     elim H0; eauto with datatypes.
     eauto with datatypes.
   Qed.
@@ -306,10 +306,10 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_inter x y) -> set_In a y.
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y.
+    simpl; tauto.
+    simpl; intros a0 l Hrec y.
     generalize (set_mem_correct1 a0 y).
-    elim (set_mem a0 y); simpl in |- *; intros.
+    elim (set_mem a0 y); simpl; intros.
     elim H0;
      [ intro Hr; rewrite <- Hr; eauto with datatypes | eauto with datatypes ].
     eauto with datatypes.
@@ -329,8 +329,8 @@ Section first_definitions.
      set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y [Ha0a| Hal] Hay.
+    simpl; tauto.
+    simpl; intros a0 l Hrec y [Ha0a| Hal] Hay.
     rewrite Ha0a; generalize (set_mem_complete2 _ _ Hay).
     elim (set_mem a y);
      [ intro Habs; discriminate Habs | auto with datatypes ].
@@ -341,8 +341,8 @@ Section first_definitions.
    forall (a:A) (x y:set), set_In a (set_diff x y) -> set_In a x.
   Proof.
     simple induction x.
-    simpl in |- *; tauto.
-    simpl in |- *; intros a0 l Hrec y; elim (set_mem a0 y).
+    simpl; tauto.
+    simpl; intros a0 l Hrec y; elim (set_mem a0 y).
     eauto with datatypes.
     intro; generalize (set_add_elim _ _ _ H).
     intros [H1| H2]; eauto with datatypes.
@@ -350,7 +350,7 @@ Section first_definitions.
 
   Lemma set_diff_elim2 :
    forall (a:A) (x y:set), set_In a (set_diff x y) -> ~ set_In a y.
-  intros a x y; elim x; simpl in |- *.
+  intros a x y; elim x; simpl.
   intros; contradiction.
   intros a0 l Hrec.
   apply set_mem_ind2; auto.
@@ -359,7 +359,7 @@ Section first_definitions.
   Qed.
 
   Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
-  red in |- *; intros a x H.
+  red; intros a x H.
   apply (set_diff_elim2 _ _ _ H).
   apply (set_diff_elim1 _ _ _ H).
   Qed.
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.