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

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e264ccb5d..e579010ba 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -24,14 +24,14 @@ Definition gtof (a b:A) := f b > f a.
 
 Theorem well_founded_ltof : well_founded ltof.
 Proof.
-  red in |- *.
+  red.
   cut (forall n (a:A), f a < n -> Acc ltof a).
   intros H a; apply (H (S (f a))); auto with arith.
   induction n.
   intros; absurd (f a < 0); auto with arith.
   intros a ltSma.
   apply Acc_intro.
-  unfold ltof in |- *; intros b ltfafb.
+  unfold ltof; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
 Defined.
@@ -73,7 +73,7 @@ Proof.
   intros; absurd (f a < 0); auto with arith.
   intros a ltSma.
   apply F.
-  unfold ltof in |- *; intros b ltfafb.
+  unfold ltof; intros b ltfafb.
   apply IHn.
   apply lt_le_trans with (f a); auto with arith.
 Defined.
@@ -108,7 +108,7 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y.
 
 Theorem well_founded_lt_compat : well_founded R.
 Proof.
-  red in |- *.
+  red.
   cut (forall n (a:A), f a < n -> Acc R a).
   intros H a; apply (H (S (f a))); auto with arith.
   induction n.
@@ -161,8 +161,8 @@ Lemma lt_wf_double_rec :
      (forall p q, p < n -> P p q) ->
      (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-  intros P Hrec p; pattern p in |- *; apply lt_wf_rec.
-  intros n H q; pattern q in |- *; apply lt_wf_rec; auto with arith.
+  intros P Hrec p; pattern p; apply lt_wf_rec.
+  intros n H q; pattern q; apply lt_wf_rec; auto with arith.
 Defined.
 
 Lemma lt_wf_double_ind :
@@ -171,8 +171,8 @@ Lemma lt_wf_double_ind :
       (forall p (q:nat), p < n -> P p q) ->
       (forall p, p < m -> P n p) -> P n m) -> forall n m, P n m.
 Proof.
-  intros P Hrec p; pattern p in |- *; apply lt_wf_ind.
-  intros n H q; pattern q in |- *; apply lt_wf_ind; auto with arith.
+  intros P Hrec p; pattern p; apply lt_wf_ind.
+  intros n H q; pattern q; apply lt_wf_ind; auto with arith.
 Qed.
 
 Hint Resolve lt_wf: arith.
@@ -190,7 +190,7 @@ Section LT_WF_REL.
   Remark acc_lt_rel : forall x:A, (exists n, F x n) -> Acc R x.
   Proof.
     intros x [n fxn]; generalize dependent x.
-    pattern n in |- *; apply lt_wf_ind; intros.
+    pattern n; apply lt_wf_ind; intros.
     constructor; intros.
     destruct (F_compat y x) as (x0,H1,H2); trivial.
     apply (H x0); auto.