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

18 files changed, 92 insertions, 92 deletions

diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
index 6866f19ae4..3c3bf3753c 100644
--- a/test-suite/failure/Uminus.v
+++ b/test-suite/failure/Uminus.v
@@ -31,7 +31,7 @@ Lemma Omega : forall i:U -> prop, induct i -> up (i WF).
 Proof.
 intros i y.
 apply y.
-unfold le, WF, induct in |- *.
+unfold le, WF, induct.
 intros x H0.
 apply y.
 exact H0.
@@ -39,7 +39,7 @@ Qed.
 
 Lemma lemma1 : induct (fun u => down (I u)).
 Proof.
-unfold induct in |- *.
+unfold induct.
 intros x p.
 intro q.
 apply (q (fun u => down (I u)) p).
diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v
index 129c380ed9..a24beaa2eb 100644
--- a/test-suite/failure/pattern.v
+++ b/test-suite/failure/pattern.v
@@ -6,4 +6,4 @@ Variable P : forall m : nat, m = n -> Prop.
 
 Goal forall p : n = n, P n p.
 intro.
-pattern n, p in |- *.
+pattern n, p.
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index addd3b459f..48fc2fffa8 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -104,7 +104,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -122,7 +122,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -158,7 +158,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -174,7 +174,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -185,10 +185,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -230,10 +230,10 @@ intros.
 change
   match i0' X1 R1, i0' X2 R2 with
   | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index 034b7f0947..a8b5b975be 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -106,7 +106,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -124,7 +124,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -160,7 +160,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -176,7 +176,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -187,10 +187,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -231,10 +231,10 @@ intros.
 change
   match i0 X1 R1, i0 X2 R2 with
   | i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 1f96ab34a2..7b62a0c56f 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -37,7 +37,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -90,7 +90,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -108,7 +108,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -144,7 +144,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -160,7 +160,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -171,10 +171,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -222,10 +222,10 @@ intros.
 change
   match i0 X1 R1, i0 X2 R2 with
   | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
index 2b38868743..58e339b4c2 100644
--- a/test-suite/misc/berardi_test.v
+++ b/test-suite/misc/berardi_test.v
@@ -45,7 +45,7 @@ Lemma AC_IF :
    (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
 Proof.
 intros P B e1 e2 Q p1 p2.
-unfold IFProp in |- *.
+unfold IFProp.
 case (EM B); assumption.
 Qed.
 
@@ -76,7 +76,7 @@ Record retract_cond : Prop :=
 Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
 Proof.
 intros r.
-case r; simpl in |- *.
+case r; simpl.
 trivial.
 Qed.
 
@@ -113,7 +113,7 @@ Lemma retract_pow_U_U : retract (pow U) U.
 Proof.
 exists g f.
 intro a.
-unfold f, g in |- *; simpl in |- *.
+unfold f, g; simpl.
 apply AC.
 exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
@@ -130,8 +130,8 @@ Definition R : U := g (fun u:U => Not_b (u U u)).
 
 Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
-unfold R at 1 in |- *.
-unfold g in |- *.
+unfold R at 1.
+unfold g.
 rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
 trivial.
 exists (fun x:pow U => x) (fun x:pow U => x); trivial.
@@ -141,7 +141,7 @@ Qed.
 Theorem classical_proof_irrelevence : T = F.
 Proof.
 generalize not_has_fixpoint.
-unfold Not_b in |- *.
+unfold Not_b.
 apply AC_IF.
 intros is_true is_false.
 elim is_true; elim is_false; trivial.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 71d331772a..6198f29a0d 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -27,13 +27,13 @@ Module Pair (X: PO) (Y: PO) <: PO.
   Qed.
 
   Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
-    unfold le in |- *;  intuition; info  eauto.
+    unfold le;  intuition; info  eauto.
   Qed.
 
   Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
     destruct p1.
     destruct p2.
-    unfold le in |- *.
+    unfold le.
      intuition.
      cutrewrite (t = t1).
      cutrewrite (t0 = t2).
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index e3694b818d..341805a16b 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -66,7 +66,7 @@ Module FuncDict (E: ELEM).
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
     intros.
-    unfold find, add in |- *.
+    unfold find, add.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -77,13 +77,13 @@ Module FuncDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    unfold add, find in |- *.
+    unfold add, find.
     cut (exists x : _, E.eq_dec e' e = right _ x).
     intros.
     elim H0.
     intros.
      rewrite H1.
-    unfold ifte in |- *.
+    unfold ifte.
     reflexivity.
 
     apply Disequality_provable.
@@ -123,7 +123,7 @@ Module Lemmas (G: SET) (E: ELEM).
    forall a : E.T, ESet.find a S1 = ESet.find a S2.
 
     intros.
-    unfold S1, S2 in |- *.
+    unfold S1, S2.
     elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
      try  rewrite <- H1; try  rewrite <- H2;
      repeat
@@ -153,7 +153,7 @@ Module ListDict (E: ELEM).
 
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -165,11 +165,11 @@ Module ListDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Disequality_provable _ _ _ H (E.eq_dec e e')).
     intros.
      rewrite H0.
-    simpl in |- *.
+    simpl.
     reflexivity.
   Qed.
 
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index b17adef678..ccce3bbe10 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -9,7 +9,7 @@ Functional Scheme iszero_ind := Induction for iszero Sort Prop.
 
 Lemma toto : forall n : nat, n = 0 -> iszero n = true.
 intros x eg.
- functional induction iszero x; simpl in |- *.
+ functional induction iszero x; simpl.
 trivial.
 inversion eg.
 Qed.
@@ -212,19 +212,19 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
 
 Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
 intros a b.
- functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
+ functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
 Qed.
 
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
+ functional induction nat_equal_bool n m; simpl; intros hyp; auto.
 rewrite <- hyp in y; simpl in y;tauto.
 inversion hyp.
 Qed.
 
 Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
+ functional induction nat_equal_bool n m; simpl; intros eg; auto.
 inversion eg.
 inversion eg.
 Qed.
@@ -245,7 +245,7 @@ Qed.
 
 Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
 intros n.
-unfold plus in |- *.
+unfold plus.
  functional induction plus n 0; intros.
 auto with arith.
 apply le_n_S.
@@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat :=
 
 Lemma princ_mod2 : forall n : nat, mod2 n <= n.
 intros n.
- functional induction mod2 n; simpl in |- *; auto with arith.
+ functional induction mod2 n; simpl; auto with arith.
 Qed.
 
 Function isfour (n : nat) : bool :=
@@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool :=
 
 Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
 intros n.
- functional induction isononeorfour n; intros istr; simpl in |- *;
+ functional induction isononeorfour n; intros istr; simpl;
  inversion istr.
 apply istrue0.
 destruct n. inversion istr.
@@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat :=
 
 Lemma test2' : forall n m : nat, ftest2 n m <= 2.
 intros n m.
- functional induction ftest2 n m; simpl in |- *; intros; auto.
+ functional induction ftest2 n m; simpl; intros; auto.
 Qed.
 
 Function ftest3 (n m : nat) {struct n} : nat :=
@@ -387,7 +387,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -408,7 +408,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -451,7 +451,7 @@ Qed.
 
 Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
 intros n m.
- functional induction ftest6 n m; simpl in |- *; auto.
+ functional induction ftest6 n m; simpl; auto.
 Qed.
 
 (* Some tests with modules *)
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
index 89b3032c02..c2d5cb2f47 100644
--- a/test-suite/success/Reg.v
+++ b/test-suite/success/Reg.v
@@ -39,7 +39,7 @@ Lemma essai7 :
  derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1.
 reg.
 apply Rlt_0_1.
-red in |- *; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
+red; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
  assumption.
 Qed.
 
@@ -127,7 +127,7 @@ Lemma essai23 :
    (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1.
 reg.
 left; apply Rlt_0_1.
-right; unfold Rminus in |- *;  rewrite Rplus_opp_r; reflexivity.
+right; unfold Rminus;  rewrite Rplus_opp_r; reflexivity.
 Qed.
 
 Lemma essai24 :
@@ -135,8 +135,8 @@ Lemma essai24 :
 reg.
  replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R.
 apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ].
-unfold Rsqr in |- *;  ring.
-red in |- *; intro; cut (0 < x * x + 1)%R.
+unfold Rsqr;  ring.
+red; intro; cut (0 < x * x + 1)%R.
 intro;  rewrite H in H0; elim (Rlt_irrefl _ H0).
 apply Rplus_le_lt_0_compat;
  [  replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ]
diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v
index b356f277c3..361c787e25 100644
--- a/test-suite/success/Try.v
+++ b/test-suite/success/Try.v
@@ -2,7 +2,7 @@
    non-existent names in Unfold [cf bug #263] *)
 
 Lemma lem1 : True.
-try unfold i_dont_exist in |- *.
+try unfold i_dont_exist.
 trivial.
 Qed.
 
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index c65cf3036c..7bed7ecb15 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -14,7 +14,7 @@ Abort.
 (* Check the combination of at, with and in (see bug #2146) *)
 
 Goal 3=3 -> 3=3. intro H.
-change 3 at 2 with (1+2) in |- *.
+change 3 at 2 with (1+2).
 change 3 at 2 with (1+2) in H |-.
 change 3 with (1+2) in H at 1 |- * at 1.
 (* Now check that there are no more 3's *)
@@ -25,10 +25,10 @@ Qed.
 change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in *.
 change 3 at 1 with (1+2) in H at 2 |-.
-change 3 at 1 with (1+2) in |- * at 3.
+change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
-change 3 in |- * at 1.
+change 3 at 1.
  *)
 
 (* Test that pretyping checks allowed elimination sorts *)
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 23e3caf8a3..8623f71868 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -16,9 +16,9 @@ intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
  generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq).
 intros H' H'0 H'1; right; right; auto.
-intros H' H'0 H'1; left; unfold rlt in |- *.
+intros H' H'0 H'1; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
-intros H' H'0 H'1; right; left; unfold rlt in |- *.
+intros H' H'0 H'1; right; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
 apply H'0; auto.
 Defined.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 01ebfc4f04..8ed941f864 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -46,21 +46,21 @@ Qed.
 
 Goal forall x, S x = S (S x).   
 intros.
-induction (S _) in |- * at -2.
+induction (S _) at -2.
 now_show (0=1).
 Undo 2.
-induction (S _) in |- * at 1 3.
+induction (S _) at 1 3.
 now_show (0=1).
 Undo 2.
-induction (S _) in |- * at 1.
+induction (S _) at 1.
 now_show (0=S (S x)).
 Undo 2.
-induction (S _) in |- * at 2.
+induction (S _) at 2.
 now_show (S x=0).
 Undo 2.
-induction (S _) in |- * at 3.
+induction (S _) at 3.
 now_show (S x=1).
 Undo 2.
-Fail induction (S _) in |- * at 4.
+Fail induction (S _) at 4.
 Abort.
 
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0c8a181673..1edddcfd74 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -2,7 +2,7 @@
 
 (* Submitted by Pierre Crégut *)
 (* Checks substitution of x *)
-Ltac f x := unfold x in |- *; idtac.
+Ltac f x := unfold x; idtac.
 
 Lemma lem1 : 0 + 0 = 0.
 f plus.
@@ -86,7 +86,7 @@ assert t.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -105,7 +105,7 @@ sym'.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -193,7 +193,7 @@ Abort.
 (* Used to fail in V8.1 *)
 
 Tactic Notation "test" constr(t) integer(n) :=
-   set (k := t) in |- * at n.
+   set (k := t) at n.
 
 Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 3241e1339b..5f8ed03d3f 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -4,5 +4,5 @@ Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
 intros.
 Fail remember nat as X.
 Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
-Fail remember nat as X in |- *.
+Fail remember nat as X.
 Abort.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 19693d70c9..653b5bf9a5 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
 Lemma setoid_set : Setoid_Theory set same.
 
-unfold same in |- *; split ; red.
-red in |- *; auto.
+unfold same; split ; red.
+red; auto.
 
-red in |- *.
+red.
 intros.
 elim (H a); auto.
 
@@ -33,19 +33,19 @@ Qed.
 Add Setoid set same setoid_set as setsetoid.
 
 Add Morphism In : In_ext.
-unfold same in |- *; intros a s t H; elim (H a); auto.
+unfold same; intros a s t H; elim (H a); auto.
 Qed.
 
 Lemma add_aux :
  forall s t : set,
  same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
-unfold same in |- *; simple induction 2; intros.
+unfold same; simple induction 2; intros.
 rewrite H1.
-simpl in |- *; left; reflexivity.
+simpl; left; reflexivity.
 
 elim (H a).
 intros.
-simpl in |- *; right.
+simpl; right.
 apply (H2 H1).
 Qed.
 
@@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty.
 
 auto.
 
-unfold same in |- *.
+unfold same.
 split.
-simpl in |- *.
+simpl.
 case (eq_dec a a).
 intros e ff; elim ff.
 
 intros; absurd (a = a); trivial.
 
-simpl in |- *.
+simpl.
 intro H; elim H.
 Qed.
 
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 469cbeb74d..e00701fb68 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -16,7 +16,7 @@ auto.
 Qed.
 
 Lemma lem3 : forall P : Prop, P.
-intro P; pattern P in |- *.
+intro P; pattern P.
 apply lem2.
 Abort.
 
@@ -34,7 +34,7 @@ Require Import Relations.
 
 Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X).
 Proof.
-  unfold transitive in |- *.
+  unfold transitive.
   intros X f g h H1 H2.
   inversion H1.
 Abort.