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

5 files changed, 33 insertions, 33 deletions

diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
index 6866f19ae..3c3bf3753 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 129c380ed..a24beaa2e 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 addd3b459..48fc2fffa 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 034b7f094..a8b5b975b 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 1f96ab34a..7b62a0c56 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'.