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

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 2f58201f7..cc8c478ab 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -52,8 +52,8 @@ Proof. exact Rlt_irrefl. Qed.
 
 Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
 Proof.
-  red in |- *; intros r1 r2 H H0; apply (Rlt_irrefl r1).
-  pattern r1 at 2 in |- *; rewrite H0; trivial.
+  red; intros r1 r2 H H0; apply (Rlt_irrefl r1).
+  pattern r1 at 2; rewrite H0; trivial.
 Qed.
 
 Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2.
@@ -104,7 +104,7 @@ Qed.
 
 Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
 Proof.
-  intros; red in |- *; tauto.
+  intros; red; tauto.
 Qed.
 Hint Resolve Rlt_le: real.
 
@@ -116,14 +116,14 @@ Qed.
 (**********)
 Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
 Proof.
-  destruct 1; red in |- *; auto with real.
+  destruct 1; red; auto with real.
 Qed.
 Hint Immediate Rle_ge: real.
 Hint Resolve Rle_ge: rorders.
 
 Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
 Proof.
-  destruct 1; red in |- *; auto with real.
+  destruct 1; red; auto with real.
 Qed.
 Hint Resolve Rge_le: real.
 Hint Immediate Rge_le: rorders.
@@ -145,7 +145,7 @@ Hint Immediate Rgt_lt: rorders.
 
 Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
 Proof.
-  intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto.
+  intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle; tauto.
 Qed.
 Hint Immediate Rnot_le_lt: real.
 
@@ -176,7 +176,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed.
 (**********)
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
-  generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
+  generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle.
   unfold not; intuition eauto 3.
 Qed.
 Hint Immediate Rlt_not_le: real.
@@ -194,7 +194,7 @@ Proof. exact Rlt_not_ge. Qed.
 Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
 Proof.
   intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2).
-  unfold Rle in |- *; intuition.
+  unfold Rle; intuition.
 Qed.
 
 Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2.
@@ -209,25 +209,25 @@ Proof. do 2 intro; apply Rge_not_lt. Qed.
 (**********)
 Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
 Proof.
-  unfold Rle in |- *; tauto.
+  unfold Rle; tauto.
 Qed.
 Hint Immediate Req_le: real.
 
 Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
 Proof.
-  unfold Rge in |- *; tauto.
+  unfold Rge; tauto.
 Qed.
 Hint Immediate Req_ge: real.
 
 Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
 Proof.
-  unfold Rle in |- *; auto.
+  unfold Rle; auto.
 Qed.
 Hint Immediate Req_le_sym: real.
 
 Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
 Proof.
-  unfold Rge in |- *; auto.
+  unfold Rge; auto.
 Qed.
 Hint Immediate Req_ge_sym: real.
 
@@ -242,7 +242,7 @@ Proof. do 2 intro; apply Rlt_asym. Qed.
 
 Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
 Proof.
-  intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition.
+  intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle; intuition.
 Qed.
 Hint Resolve Rle_antisym: real.
 
@@ -293,13 +293,13 @@ Proof. eauto using Rlt_trans with rorders. Qed.
 Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
 Proof.
   generalize Rlt_trans Rlt_eq_compat.
-  unfold Rle in |- *.
+  unfold Rle.
   intuition eauto 2.
 Qed.
 
 Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
 Proof.
-  generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2.
+  generalize Rlt_trans Rlt_eq_compat; unfold Rle; intuition eauto 2.
 Qed.
 
 Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
@@ -432,7 +432,7 @@ Hint Resolve Rplus_eq_reg_l: real.
 (**********)
 Lemma Rplus_0_r_uniq : forall r r1, r + r1 = r -> r1 = 0.
 Proof.
-  intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real.
+  intros r b; pattern r at 2; replace r with (r + 0); eauto with real.
 Qed.
 
 (***********)
@@ -443,7 +443,7 @@ Proof.
     absurd (0 < a + b).
       rewrite H1; auto with real.
       apply Rle_lt_trans with (a + 0).
-        rewrite Rplus_0_r in |- *; assumption.
+        rewrite Rplus_0_r; assumption.
         auto using Rplus_lt_compat_l with real.
     rewrite <- H0, Rplus_0_r in H1; assumption.
 Qed.
@@ -572,14 +572,14 @@ Qed.
 (**********)
 Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
 Proof.
-  intros r1 r2 H; split; red in |- *; intro; apply H; auto with real.
+  intros r1 r2 H; split; red; intro; apply H; auto with real.
 Qed.
 
 (**********)
 Lemma Rmult_integral_contrapositive :
   forall r1 r2, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0.
 Proof.
-  red in |- *; intros r1 r2 [H1 H2] H.
+  red; intros r1 r2 [H1 H2] H.
   case (Rmult_integral r1 r2); auto with real.
 Qed.
 Hint Resolve Rmult_integral_contrapositive: real.
@@ -606,12 +606,12 @@ Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope.
 
 (***********)
 Lemma Rsqr_0 : Rsqr 0 = 0.
-  unfold Rsqr in |- *; auto with real.
+  unfold Rsqr; auto with real.
 Qed.
 
 (***********)
 Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0.
-  unfold Rsqr in |- *; intros; elim (Rmult_integral r r H); trivial.
+  unfold Rsqr; intros; elim (Rmult_integral r r H); trivial.
 Qed.
 
 (*********************************************************)
@@ -649,7 +649,7 @@ Hint Resolve Ropp_involutive: real.
 (*********)
 Lemma Ropp_neq_0_compat : forall r, r <> 0 -> - r <> 0.
 Proof.
-  red in |- *; intros r H H0.
+  red; intros r H H0.
   apply H.
   transitivity (- - r); auto with real.
 Qed.
@@ -722,7 +722,7 @@ Hint Resolve Rminus_diag_eq: real.
 (**********)
 Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 = 0 -> r1 = r2.
 Proof.
-  intros r1 r2; unfold Rminus in |- *; rewrite Rplus_comm; intro.
+  intros r1 r2; unfold Rminus; rewrite Rplus_comm; intro.
   rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
 Qed.
 Hint Immediate Rminus_diag_uniq: real.
@@ -743,20 +743,20 @@ Hint Resolve Rplus_minus: real.
 (**********)
 Lemma Rminus_eq_contra : forall r1 r2, r1 <> r2 -> r1 - r2 <> 0.
 Proof.
-  red in |- *; intros r1 r2 H H0.
+  red; intros r1 r2 H H0.
   apply H; auto with real.
 Qed.
 Hint Resolve Rminus_eq_contra: real.
 
 Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2.
 Proof.
-  red in |- *; intros; elim H; apply Rminus_diag_eq; auto.
+  red; intros; elim H; apply Rminus_diag_eq; auto.
 Qed.
 Hint Resolve Rminus_not_eq: real.
 
 Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
 Proof.
-  red in |- *; intros; elim H; rewrite H0; ring.
+  red; intros; elim H; rewrite H0; ring.
 Qed.
 Hint Resolve Rminus_not_eq_right: real.
 
@@ -780,7 +780,7 @@ Hint Resolve Rinv_1: real.
 (*********)
 Lemma Rinv_neq_0_compat : forall r, r <> 0 -> / r <> 0.
 Proof.
-  red in |- *; intros; apply R1_neq_R0.
+  red; intros; apply R1_neq_R0.
   replace 1 with (/ r * r); auto with real.
 Qed.
 Hint Resolve Rinv_neq_0_compat: real.
@@ -860,7 +860,7 @@ Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
 (**********)
 Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
 Proof.
-  unfold Rle in |- *; intros; elim H; intro.
+  unfold Rle; intros; elim H; intro.
   left; apply (Rplus_lt_compat_l r r1 r2 H0).
   right; rewrite <- H0; auto with zarith real.
 Qed.
@@ -872,7 +872,7 @@ Hint Resolve Rplus_ge_compat_l: real.
 (**********)
 Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.
 Proof.
-  unfold Rle in |- *; intros; elim H; intro.
+  unfold Rle; intros; elim H; intro.
   left; apply (Rplus_lt_compat_r r r1 r2 H0).
   right; rewrite <- H0; auto with real.
 Qed.
@@ -933,7 +933,7 @@ Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
 Proof.
   intros x y; intros; apply Rlt_trans with x;
     [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
         assumption ].
 Qed.
 
@@ -941,7 +941,7 @@ Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
 Proof.
   intros x y; intros; apply Rle_lt_trans with x;
     [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
         assumption ].
 Qed.
 
@@ -955,7 +955,7 @@ Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
 Proof.
   intros x y; intros; apply Rle_trans with x;
     [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
         assumption ].
 Qed.
 
@@ -983,7 +983,7 @@ Qed.
 
 Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
 Proof.
-  unfold Rle in |- *; intros; elim H; intro.
+  unfold Rle; intros; elim H; intro.
   left; apply (Rplus_lt_reg_r r r1 r2 H0).
   right; apply (Rplus_eq_reg_l r r1 r2 H0).
 Qed.
@@ -997,7 +997,7 @@ Qed.
 
 Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
 Proof.
-  unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H).
+  unfold Rgt; intros; apply (Rplus_lt_reg_r r r2 r1 H).
 Qed.
 
 Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
@@ -1048,7 +1048,7 @@ Qed.
 
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
-  unfold Rgt in |- *; intros.
+  unfold Rgt; intros.
   apply (Rplus_lt_reg_r (r2 + r1)).
   replace (r2 + r1 + - r1) with r2.
   replace (r2 + r1 + - r2) with r1.
@@ -1060,7 +1060,7 @@ Hint Resolve Ropp_gt_lt_contravar.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
-  unfold Rgt in |- *; auto with real.
+  unfold Rgt; auto with real.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: real.
 
@@ -1185,7 +1185,7 @@ Proof. eauto using Rmult_lt_compat_l with rorders. Qed.
 Lemma Rmult_le_compat_l :
   forall r r1 r2, 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
 Proof.
-  intros r r1 r2 H H0; destruct H; destruct H0; unfold Rle in |- *;
+  intros r r1 r2 H H0; destruct H; destruct H0; unfold Rle;
     auto with real.
   right; rewrite <- H; do 2 rewrite Rmult_0_l; reflexivity.
 Qed.
@@ -1344,7 +1344,7 @@ Qed.
 (**********)
 Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
 Proof.
-  destruct 1; unfold Rle in |- *; auto with real.
+  destruct 1; unfold Rle; auto with real.
 Qed.
 
 Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
@@ -1358,7 +1358,7 @@ Qed.
 Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
 Proof.
   intros; replace r1 with (r1 - r2 + r2).
-  pattern r2 at 3 in |- *; replace r2 with (0 + r2); auto with real.
+  pattern r2 at 3; replace r2 with (0 + r2); auto with real.
   ring.
 Qed.
 
@@ -1374,7 +1374,7 @@ Qed.
 Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
 Proof.
   intros; replace r1 with (r1 - r2 + r2).
-  pattern r2 at 3 in |- *; replace r2 with (0 + r2); auto with real.
+  pattern r2 at 3; replace r2 with (0 + r2); auto with real.
   ring.
 Qed.
 
@@ -1400,7 +1400,7 @@ Hint Immediate tech_Rplus: real.
 
 Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.
 Proof.
-  intro; case (Rlt_le_dec r 0); unfold Rsqr in |- *; intro.
+  intro; case (Rlt_le_dec r 0); unfold Rsqr; intro.
   replace (r * r) with (- r * - r); auto with real.
   replace 0 with (- r * 0); auto with real.
   replace 0 with (0 * r); auto with real.
@@ -1409,7 +1409,7 @@ Qed.
 (***********)
 Lemma Rlt_0_sqr : forall r, r <> 0 -> 0 < Rsqr r.
 Proof.
-  intros; case (Rdichotomy r 0); trivial; unfold Rsqr in |- *; intro.
+  intros; case (Rdichotomy r 0); trivial; unfold Rsqr; intro.
   replace (r * r) with (- r * - r); auto with real.
   replace 0 with (- r * 0); auto with real.
   replace 0 with (0 * r); auto with real.
@@ -1439,7 +1439,7 @@ Qed.
 Lemma Rlt_0_1 : 0 < 1.
 Proof.
   replace 1 with (Rsqr 1); auto with real.
-  unfold Rsqr in |- *; auto with real.
+  unfold Rsqr; auto with real.
 Qed.
 Hint Resolve Rlt_0_1: real.
 
@@ -1455,7 +1455,7 @@ Qed.
 
 Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
 Proof.
-  intros; apply Rnot_le_lt; red in |- *; intros.
+  intros; apply Rnot_le_lt; red; intros.
   absurd (1 <= 0); auto with real.
   replace 1 with (r * / r); auto with real.
   replace 0 with (r * 0); auto with real.
@@ -1465,7 +1465,7 @@ Hint Resolve Rinv_0_lt_compat: real.
 (*********)
 Lemma Rinv_lt_0_compat : forall r, r < 0 -> / r < 0.
 Proof.
-  intros; apply Rnot_le_lt; red in |- *; intros.
+  intros; apply Rnot_le_lt; red; intros.
   absurd (1 <= 0); auto with real.
   replace 1 with (r * / r); auto with real.
   replace 0 with (r * 0); auto with real.
@@ -1479,8 +1479,8 @@ Proof.
   case (Rmult_neq_0_reg r1 r2); intros; auto with real.
   replace (r1 * r2 * / r2) with r1.
   replace (r1 * r2 * / r1) with r2; trivial.
-  symmetry  in |- *; auto with real.
-  symmetry  in |- *; auto with real.
+  symmetry ; auto with real.
+  symmetry ; auto with real.
 Qed.
 
 Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1.
@@ -1497,7 +1497,7 @@ Proof.
   rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite (Rmult_comm y (/ y));
     rewrite Rinv_l; auto with real.
   apply Rlt_dichotomy_converse; right.
-  red in |- *; apply Rlt_trans with (r2 := x); auto with real.
+  red; apply Rlt_trans with (r2 := x); auto with real.
 Qed.
 Hint Resolve Rinv_1_lt_contravar: real.
 
@@ -1510,7 +1510,7 @@ Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
 Proof.
   intros.
   apply Rlt_le_trans with 1; auto with real.
-  pattern 1 at 1 in |- *; replace 1 with (0 + 1); auto with real.
+  pattern 1 at 1; replace 1 with (0 + 1); auto with real.
 Qed.
 Hint Resolve Rle_lt_0_plus_1: real.
 
@@ -1518,15 +1518,15 @@ Hint Resolve Rle_lt_0_plus_1: real.
 Lemma Rlt_plus_1 : forall r, r < r + 1.
 Proof.
   intros.
-  pattern r at 1 in |- *; replace r with (r + 0); auto with real.
+  pattern r at 1; replace r with (r + 0); auto with real.
 Qed.
 Hint Resolve Rlt_plus_1: real.
 
 (**********)
 Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2.
 Proof.
-  red in |- *; unfold Rminus in |- *; intros.
-  pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real.
+  red; unfold Rminus; intros.
+  pattern r1 at 2; replace r1 with (r1 + 0); auto with real.
 Qed.
 
 (*********************************************************)
@@ -1542,14 +1542,14 @@ Qed.
 (**********)
 Lemma S_O_plus_INR : forall n:nat, INR (1 + n) = INR 1 + INR n.
 Proof.
-  intro; simpl in |- *; case n; intros; auto with real.
+  intro; simpl; case n; intros; auto with real.
 Qed.
 
 (**********)
 Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
 Proof.
   intros n m; induction  n as [| n Hrecn].
-  simpl in |- *; auto with real.
+  simpl; auto with real.
   replace (S n + m)%nat with (S (n + m)); auto with arith.
   repeat rewrite S_INR.
   rewrite Hrecn; ring.
@@ -1559,9 +1559,9 @@ Hint Resolve plus_INR: real.
 (**********)
 Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) = INR n - INR m.
 Proof.
-  intros n m le; pattern m, n in |- *; apply le_elim_rel; auto with real.
+  intros n m le; pattern m, n; apply le_elim_rel; auto with real.
   intros; rewrite <- minus_n_O; auto with real.
-  intros; repeat rewrite S_INR; simpl in |- *.
+  intros; repeat rewrite S_INR; simpl.
   rewrite H0; ring.
 Qed.
 Hint Resolve minus_INR: real.
@@ -1570,8 +1570,8 @@ Hint Resolve minus_INR: real.
 Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m.
 Proof.
   intros n m; induction  n as [| n Hrecn].
-  simpl in |- *; auto with real.
-  intros; repeat rewrite S_INR; simpl in |- *.
+  simpl; auto with real.
+  intros; repeat rewrite S_INR; simpl.
   rewrite plus_INR; rewrite Hrecn; ring.
 Qed.
 Hint Resolve mult_INR: real.
@@ -1602,7 +1602,7 @@ Hint Resolve lt_1_INR: real.
 Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p).
 Proof.
   intro; apply lt_0_INR.
-  simpl in |- *; auto with real.
+  simpl; auto with real.
   apply Pos2Nat.is_pos.
 Qed.
 Hint Resolve pos_INR_nat_of_P: real.
@@ -1611,7 +1611,7 @@ Hint Resolve pos_INR_nat_of_P: real.
 Lemma pos_INR : forall n:nat, 0 <= INR n.
 Proof.
   intro n; case n.
-  simpl in |- *; auto with real.
+  simpl; auto with real.
   auto with arith real.
 Qed.
 Hint Resolve pos_INR: real.
@@ -1619,10 +1619,10 @@ Hint Resolve pos_INR: real.
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
 Proof.
   double induction n m; intros.
-  simpl in |- *; exfalso; apply (Rlt_irrefl 0); auto.
+  simpl; exfalso; apply (Rlt_irrefl 0); auto.
   auto with arith.
   generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
-    [ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
+    [ intro H2; rewrite H2 in H0; idtac | simpl; trivial ].
   generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso;
     apply (Rlt_irrefl 0); auto.
   do 2 rewrite S_INR in H1; cut (INR n1 < INR n0).
@@ -1644,7 +1644,7 @@ Hint Resolve le_INR: real.
 (**********)
 Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
 Proof.
-  red in |- *; intros n H H1.
+  red; intros n H H1.
   apply H.
   rewrite H1; trivial.
 Qed.
@@ -1656,7 +1656,7 @@ Proof.
   intro n; case n.
   intro; absurd (0%nat = 0%nat); trivial.
   intros; rewrite S_INR.
-  apply Rgt_not_eq; red in |- *; auto with real.
+  apply Rgt_not_eq; red; auto with real.
 Qed.
 Hint Resolve not_0_INR: real.
 
@@ -1677,7 +1677,7 @@ Proof.
   cut (n <> m).
   intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto.
   omega.
-  symmetry  in |- *; cut (m <> n).
+  symmetry ; cut (m <> n).
   intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto.
   omega.
 Qed.
@@ -1712,7 +1712,7 @@ Qed.
 Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z.of_nat n).
 Proof.
   simple induction n; auto with real.
-  intros; simpl in |- *; rewrite SuccNat2Pos.id_succ;
+  intros; simpl; rewrite SuccNat2Pos.id_succ;
     auto with real.
 Qed.
 
@@ -1744,7 +1744,7 @@ Qed.
 (**********)
 Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m.
 Proof.
-  intros z t; case z; case t; simpl in |- *; auto with real.
+  intros z t; case z; case t; simpl; auto with real.
   intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
   intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real.
   rewrite Rmult_comm.
@@ -1775,7 +1775,7 @@ Qed.
 (**********)
 Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
-  intro z; case z; simpl in |- *; auto with real.
+  intro z; case z; simpl; auto with real.
 Qed.
 
 Definition Ropp_Ropp_IZR := opp_IZR.
@@ -1790,16 +1790,16 @@ Qed.
 (**********)
 Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
 Proof.
-  intros z1 z2; unfold Rminus in |- *; unfold Z.sub in |- *.
-  rewrite <- (Ropp_Ropp_IZR z2); symmetry  in |- *; apply plus_IZR.
+  intros z1 z2; unfold Rminus; unfold Z.sub.
+  rewrite <- (Ropp_Ropp_IZR z2); symmetry ; apply plus_IZR.
 Qed.
 
 (**********)
 Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
 Proof.
-  intro z; case z; simpl in |- *; intros.
+  intro z; case z; simpl; intros.
   absurd (0 < 0); auto with real.
-  unfold Z.lt in |- *; simpl in |- *; trivial.
+  unfold Z.lt; simpl; trivial.
   case Rlt_not_le with (1 := H).
   replace 0 with (-0); auto with real.
 Qed.
@@ -1816,10 +1816,10 @@ Qed.
 (**********)
 Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z.
 Proof.
-  intro z; destruct z; simpl in |- *; intros; auto with zarith.
+  intro z; destruct z; simpl; intros; auto with zarith.
   case (Rlt_not_eq 0 (INR (Pos.to_nat p))); auto with real.
   case (Rlt_not_eq (- INR (Pos.to_nat p)) 0); auto with real.
-  apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply pos_INR_nat_of_P.
+  apply Ropp_lt_gt_0_contravar. unfold Rgt; apply pos_INR_nat_of_P.
 Qed.
 
 (**********)
@@ -1833,22 +1833,22 @@ Qed.
 (**********)
 Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0.
 Proof.
-  intros z H; red in |- *; intros H0; case H.
+  intros z H; red; intros H0; case H.
   apply eq_IZR; auto.
 Qed.
 
 (*********)
 Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
 Proof.
-  unfold Rle in |- *; intros z [H| H].
-  red in |- *; intro; apply (Z.lt_le_incl 0 z (lt_0_IZR z H)); assumption.
+  unfold Rle; intros z [H| H].
+  red; intro; apply (Z.lt_le_incl 0 z (lt_0_IZR z H)); assumption.
   rewrite (eq_IZR_R0 z); auto with zarith real.
 Qed.
 
 (**********)
 Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
 Proof.
-  unfold Rle in |- *; intros z1 z2 [H| H].
+  unfold Rle; intros z1 z2 [H| H].
   apply (Z.lt_le_incl z1 z2); auto with real.
   apply lt_IZR; trivial.
   rewrite (eq_IZR z1 z2); auto with zarith real.
@@ -1857,20 +1857,20 @@ Qed.
 (**********)
 Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z.
 Proof.
-  pattern 1 at 1 in |- *; replace 1 with (IZR 1); intros; auto.
+  pattern 1 at 1; replace 1 with (IZR 1); intros; auto.
   apply le_IZR; trivial.
 Qed.
 
 (**********)
 Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
 Proof.
-  intros m n H; apply Rnot_lt_ge; red in |- *; intro.
+  intros m n H; apply Rnot_lt_ge; red; intro.
   generalize (lt_IZR m n H0); intro; omega.
 Qed.
 
 Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
 Proof.
-  intros m n H; apply Rnot_gt_le; red in |- *; intro.
+  intros m n H; apply Rnot_gt_le; red; intro.
   unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega.
 Qed.
 
@@ -1899,10 +1899,10 @@ Proof.
   apply one_IZR_lt1.
   rewrite <- Z_R_minus; split.
   replace (-1) with (r - (r + 1)).
-  unfold Rminus in |- *; apply Rplus_lt_le_compat; auto with real.
+  unfold Rminus; apply Rplus_lt_le_compat; auto with real.
   ring.
   replace 1 with (r + 1 - r).
-  unfold Rminus in |- *; apply Rplus_le_lt_compat; auto with real.
+  unfold Rminus; apply Rplus_le_lt_compat; auto with real.
   ring.
 Qed.
 
@@ -1943,8 +1943,8 @@ Proof.
   rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
     rewrite <- Rinv_l_sym.
   rewrite Rmult_1_r; apply H1.
-  red in |- *; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0).
-  red in |- *; intro; rewrite H2 in H; elim (Rlt_irrefl _ H).
+  red; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0).
+  red; intro; rewrite H2 in H; elim (Rlt_irrefl _ H).
 Qed.
 
 Lemma double : forall r1, 2 * r1 = r1 + r1.
@@ -1954,10 +1954,10 @@ Qed.
 
 Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2.
 Proof.
-  intro; rewrite <- double; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
-    symmetry  in |- *; apply Rinv_r_simpl_m.
+  intro; rewrite <- double; unfold Rdiv; rewrite <- Rmult_assoc;
+    symmetry ; apply Rinv_r_simpl_m.
   replace 2 with (INR 2);
-  [ apply not_0_INR; discriminate | unfold INR in |- *; ring ].
+  [ apply not_0_INR; discriminate | unfold INR; ring ].
 Qed.
 
 (*********************************************************)
@@ -1992,22 +1992,22 @@ Proof.
   rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
   ring.
   replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ].
-  pattern y at 2 in |- *; replace y with (y / 2 + y / 2).
-  unfold Rminus, Rdiv in |- *.
+  pattern y at 2; replace y with (y / 2 + y / 2).
+  unfold Rminus, Rdiv.
   repeat rewrite Rmult_plus_distr_r.
   ring.
   cut (forall z:R, 2 * z = z + z).
   intro.
   rewrite <- (H4 (y / 2)).
-  unfold Rdiv in |- *.
+  unfold Rdiv.
   rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
   replace 2 with (INR 2).
   apply not_0_INR.
   discriminate.
-  unfold INR in |- *; reflexivity.
+  unfold INR; reflexivity.
   intro; ring.
   cut (0%nat <> 2%nat);
-    [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR in |- *;
+    [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR;
       intro; assumption
       | discriminate ].
 Qed.