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

diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index a369d5ae2..93a889202 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -19,13 +19,13 @@ Local Open Scope R_scope.
 (**********)
 Lemma continuity_sin : continuity sin.
 Proof.
-  unfold continuity in |- *; intro.
+  unfold continuity; intro.
   assert (H0 := continuity_cos (PI / 2 - x)).
   unfold continuity_pt in H0; unfold continue_in in H0; unfold limit1_in in H0;
     unfold limit_in in H0; simpl in H0; unfold R_dist in H0;
-      unfold continuity_pt in |- *; unfold continue_in in |- *;
-        unfold limit1_in in |- *; unfold limit_in in |- *;
-          simpl in |- *; unfold R_dist in |- *; intros.
+      unfold continuity_pt; unfold continue_in;
+        unfold limit1_in; unfold limit_in;
+          simpl; unfold R_dist; intros.
   elim (H0 _ H); intros.
   exists x0; intros.
   elim H1; intros.
@@ -34,9 +34,9 @@ Proof.
   intros; rewrite <- (cos_shift x); rewrite <- (cos_shift x1); apply H3.
   elim H4; intros.
   split.
-  unfold D_x, no_cond in |- *; split.
+  unfold D_x, no_cond; split.
   trivial.
-  red in |- *; intro; unfold D_x, no_cond in H5; elim H5; intros _ H8; elim H8;
+  red; intro; unfold D_x, no_cond in H5; elim H5; intros _ H8; elim H8;
     rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive x1);
       apply Ropp_eq_compat; apply Rplus_eq_reg_l with (PI / 2);
         apply H7.
@@ -50,7 +50,7 @@ Lemma CVN_R_sin :
     (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)) ->
     CVN_R fn.
 Proof.
-  unfold CVN_R in |- *; unfold CVN_r in |- *; intros fn H r.
+  unfold CVN_R; unfold CVN_r; intros fn H r.
   exists (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)).
   cut
     { l:R |
@@ -63,7 +63,7 @@ Proof.
   exists x.
   split.
   apply p.
-  intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult;
+  intros; rewrite H; unfold Rdiv; do 2 rewrite Rabs_mult;
     rewrite pow_1_abs; rewrite Rmult_1_l.
   cut (0 < / INR (fact (2 * n + 1))).
   intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))).
@@ -80,11 +80,11 @@ Proof.
   apply Rinv_neq_0_compat; apply INR_fact_neq_0.
   apply pow_nonzero; assumption.
   assert (H1 := Alembert_sin).
-  unfold sin_n in H1; unfold Un_cv in H1; unfold Un_cv in |- *; intros.
+  unfold sin_n in H1; unfold Un_cv in H1; unfold Un_cv; intros.
   cut (0 < eps / Rsqr r).
   intro; elim (H1 _ H3); intros N0 H4.
   exists N0; intros.
-  unfold R_dist in |- *; assert (H6 := H4 _ H5).
+  unfold R_dist; assert (H6 := H4 _ H5).
   unfold R_dist in H5;
     replace
     (Rabs
@@ -96,15 +96,15 @@ Proof.
         ((-1) ^ n / INR (fact (2 * n + 1))))).
   apply Rmult_lt_reg_l with (/ Rsqr r).
   apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
-  pattern (/ Rsqr r) at 1 in |- *; rewrite <- (Rabs_right (/ Rsqr r)).
+  pattern (/ Rsqr r) at 1; rewrite <- (Rabs_right (/ Rsqr r)).
   rewrite <- Rabs_mult.
   rewrite Rmult_minus_distr_l.
   rewrite Rmult_0_r; rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
   rewrite Rmult_1_l; rewrite <- (Rmult_comm eps).
   apply H6.
-  unfold Rsqr in |- *; apply prod_neq_R0; assumption.
+  unfold Rsqr; apply prod_neq_R0; assumption.
   apply Rle_ge; left; apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption.
-  unfold Rdiv in |- *; rewrite (Rmult_comm (Rsqr r)); repeat rewrite Rabs_mult;
+  unfold Rdiv; rewrite (Rmult_comm (Rsqr r)); repeat rewrite Rabs_mult;
     rewrite Rabs_Rabsolu; rewrite pow_1_abs.
   rewrite Rmult_1_l.
   repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l.
@@ -126,10 +126,10 @@ Proof.
   replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r).
   do 2 rewrite <- Rmult_assoc.
   rewrite <- Rinv_l_sym.
-  unfold Rsqr in |- *; ring.
+  unfold Rsqr; ring.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
-  simpl in |- *; ring.
+  simpl; ring.
   ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
@@ -142,16 +142,16 @@ Proof.
   apply INR_fact_neq_0.
   apply pow_nonzero; discrR.
   apply Rinv_neq_0_compat; apply INR_fact_neq_0.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+  unfold Rdiv; apply Rmult_lt_0_compat;
     [ assumption | apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption ].
-  assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0;
+  assert (H0 := cond_pos r); red; intro; rewrite H1 in H0;
     elim (Rlt_irrefl _ H0).
 Qed.
 
 (** (sin h)/h -> 1 when h -> 0 *)
 Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1.
 Proof.
-  unfold derivable_pt_lim in |- *; intros.
+  unfold derivable_pt_lim; intros.
   set
     (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)).
   cut (CVN_R fn).
@@ -167,58 +167,58 @@ Proof.
   elim (H2 _ H); intros alp H3.
   elim H3; intros.
   exists (mkposreal _ H4).
-  simpl in |- *; intros.
-  rewrite sin_0; rewrite Rplus_0_l; unfold Rminus in |- *; rewrite Ropp_0;
+  simpl; intros.
+  rewrite sin_0; rewrite Rplus_0_l; unfold Rminus; rewrite Ropp_0;
     rewrite Rplus_0_r.
   cut (Rabs (SFL fn cv h - SFL fn cv 0) < eps).
   intro; cut (SFL fn cv 0 = 1).
   intro; cut (SFL fn cv h = sin h / h).
   intro; rewrite H9 in H8; rewrite H10 in H8.
   apply H8.
-  unfold SFL, sin in |- *.
+  unfold SFL, sin.
   case (cv h); intros.
   case (exist_sin (Rsqr h)); intros.
-  unfold Rdiv in |- *; rewrite (Rinv_r_simpl_m h x0 H6).
+  unfold Rdiv; rewrite (Rinv_r_simpl_m h x0 H6).
   eapply UL_sequence.
   apply u.
   unfold sin_in in s; unfold sin_n, infinite_sum in s;
-    unfold SP, fn, Un_cv in |- *; intros.
+    unfold SP, fn, Un_cv; intros.
   elim (s _ H10); intros N0 H11.
   exists N0; intros.
-  unfold R_dist in |- *; unfold R_dist in H11.
+  unfold R_dist; unfold R_dist in H11.
   replace
   (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * h ^ (2 * k)) n)
     with
       (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * Rsqr h ^ i) n).
   apply H11; assumption.
-  apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr in |- *;
+  apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr;
     rewrite pow_sqr; reflexivity.
-  unfold SFL, sin in |- *.
+  unfold SFL, sin.
   case (cv 0); intros.
   eapply UL_sequence.
   apply u.
-  unfold SP, fn in |- *; unfold Un_cv in |- *; intros; exists 1%nat; intros.
-  unfold R_dist in |- *;
+  unfold SP, fn; unfold Un_cv; intros; exists 1%nat; intros.
+  unfold R_dist;
     replace
     (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k)) n)
     with 1.
-  unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
+  unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
   rewrite decomp_sum.
-  simpl in |- *; rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite Rinv_1;
-    rewrite Rmult_1_r; pattern 1 at 1 in |- *; rewrite <- Rplus_0_r;
+  simpl; rewrite Rmult_1_r; unfold Rdiv; rewrite Rinv_1;
+    rewrite Rmult_1_r; pattern 1 at 1; rewrite <- Rplus_0_r;
       apply Rplus_eq_compat_l.
-  symmetry  in |- *; apply sum_eq_R0; intros.
+  symmetry ; apply sum_eq_R0; intros.
   rewrite Rmult_0_l; rewrite Rmult_0_r; reflexivity.
   unfold ge in H10; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H10 ].
   apply H5.
   split.
-  unfold D_x, no_cond in |- *; split.
+  unfold D_x, no_cond; split.
   trivial.
   apply (not_eq_sym (A:=R)); apply H6.
-  unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; apply H7.
-  unfold Boule in |- *; unfold Rminus in |- *; rewrite Ropp_0;
+  unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply H7.
+  unfold Boule; unfold Rminus; rewrite Ropp_0;
     rewrite Rplus_0_r; rewrite Rabs_R0; apply (cond_pos r).
-  intros; unfold fn in |- *;
+  intros; unfold fn;
     replace (fun x:R => (-1) ^ n / INR (fact (2 * n + 1)) * x ^ (2 * n)) with
     (fct_cte ((-1) ^ n / INR (fact (2 * n + 1))) * pow_fct (2 * n))%F;
     [ idtac | reflexivity ].
@@ -229,13 +229,13 @@ Proof.
   apply (derivable_pt_pow (2 * n) y).
   apply (X r).
   apply (CVN_R_CVS _ X).
-  apply CVN_R_sin; unfold fn in |- *; reflexivity.
+  apply CVN_R_sin; unfold fn; reflexivity.
 Qed.
 
 (** ((cos h)-1)/h -> 0 when h -> 0 *)
 Lemma derivable_pt_lim_cos_0 : derivable_pt_lim cos 0 0.
 Proof.
-  unfold derivable_pt_lim in |- *; intros.
+  unfold derivable_pt_lim; intros.
   assert (H0 := derivable_pt_lim_sin_0).
   unfold derivable_pt_lim in H0.
   cut (0 < eps / 2).
@@ -250,8 +250,8 @@ Proof.
   intro; set (delta := mkposreal _ H6).
   exists delta; intros.
   rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))).
-  unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r.
-  unfold Rdiv in |- *; do 2 rewrite Ropp_mult_distr_l_reverse.
+  unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r.
+  unfold Rdiv; do 2 rewrite Ropp_mult_distr_l_reverse.
   rewrite Rabs_Ropp.
   replace (2 * Rsqr (sin (h * / 2)) * / h) with
   (sin (h / 2) * (sin (h / 2) / (h / 2) - 1) + sin (h / 2)).
@@ -261,12 +261,12 @@ Proof.
   rewrite (double_var eps); apply Rplus_lt_compat.
   apply Rle_lt_trans with (Rabs (sin (h / 2) / (h / 2) - 1)).
   rewrite Rabs_mult; rewrite Rmult_comm;
-    pattern (Rabs (sin (h / 2) / (h / 2) - 1)) at 2 in |- *;
+    pattern (Rabs (sin (h / 2) / (h / 2) - 1)) at 2;
       rewrite <- Rmult_1_r; apply Rmult_le_compat_l.
   apply Rabs_pos.
   assert (H9 := SIN_bound (h / 2)).
-  unfold Rabs in |- *; case (Rcase_abs (sin (h / 2))); intro.
-  pattern 1 at 3 in |- *; rewrite <- (Ropp_involutive 1).
+  unfold Rabs; case (Rcase_abs (sin (h / 2))); intro.
+  pattern 1 at 3; rewrite <- (Ropp_involutive 1).
   apply Ropp_le_contravar.
   elim H9; intros; assumption.
   elim H9; intros; assumption.
@@ -275,50 +275,50 @@ Proof.
   intro; assert (H11 := H2 _ H10 H9).
   rewrite Rplus_0_l in H11; rewrite sin_0 in H11.
   rewrite Rminus_0_r in H11; apply H11.
-  unfold Rdiv in |- *; apply prod_neq_R0.
+  unfold Rdiv; apply prod_neq_R0.
   apply H7.
   apply Rinv_neq_0_compat; discrR.
   apply Rlt_trans with (del / 2).
-  unfold Rdiv in |- *; rewrite Rabs_mult.
+  unfold Rdiv; rewrite Rabs_mult.
   rewrite (Rabs_right (/ 2)).
   do 2 rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l.
   apply Rinv_0_lt_compat; prove_sup0.
   apply Rlt_le_trans with (pos delta).
   apply H8.
-  unfold delta in |- *; simpl in |- *; apply Rmin_l.
+  unfold delta; simpl; apply Rmin_l.
   apply Rle_ge; left; apply Rinv_0_lt_compat; prove_sup0.
-  rewrite <- (Rplus_0_r (del / 2)); pattern del at 1 in |- *;
+  rewrite <- (Rplus_0_r (del / 2)); pattern del at 1;
     rewrite (double_var del); apply Rplus_lt_compat_l;
-      unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+      unfold Rdiv; apply Rmult_lt_0_compat.
   apply (cond_pos del).
   apply Rinv_0_lt_compat; prove_sup0.
   elim H5; intros; assert (H11 := H10 (h / 2)).
   rewrite sin_0 in H11; do 2 rewrite Rminus_0_r in H11.
   apply H11.
   split.
-  unfold D_x, no_cond in |- *; split.
+  unfold D_x, no_cond; split.
   trivial.
-  apply (not_eq_sym (A:=R)); unfold Rdiv in |- *; apply prod_neq_R0.
+  apply (not_eq_sym (A:=R)); unfold Rdiv; apply prod_neq_R0.
   apply H7.
   apply Rinv_neq_0_compat; discrR.
   apply Rlt_trans with (del_c / 2).
-  unfold Rdiv in |- *; rewrite Rabs_mult.
+  unfold Rdiv; rewrite Rabs_mult.
   rewrite (Rabs_right (/ 2)).
   do 2 rewrite <- (Rmult_comm (/ 2)).
   apply Rmult_lt_compat_l.
   apply Rinv_0_lt_compat; prove_sup0.
   apply Rlt_le_trans with (pos delta).
   apply H8.
-  unfold delta in |- *; simpl in |- *; apply Rmin_r.
+  unfold delta; simpl; apply Rmin_r.
   apply Rle_ge; left; apply Rinv_0_lt_compat; prove_sup0.
-  rewrite <- (Rplus_0_r (del_c / 2)); pattern del_c at 2 in |- *;
+  rewrite <- (Rplus_0_r (del_c / 2)); pattern del_c at 2;
     rewrite (double_var del_c); apply Rplus_lt_compat_l.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+  unfold Rdiv; apply Rmult_lt_0_compat.
   apply H9.
   apply Rinv_0_lt_compat; prove_sup0.
-  rewrite Rmult_minus_distr_l; rewrite Rmult_1_r; unfold Rminus in |- *;
+  rewrite Rmult_minus_distr_l; rewrite Rmult_1_r; unfold Rminus;
     rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
-      rewrite (Rmult_comm 2); unfold Rdiv, Rsqr in |- *.
+      rewrite (Rmult_comm 2); unfold Rdiv, Rsqr.
   repeat rewrite Rmult_assoc.
   repeat apply Rmult_eq_compat_l.
   rewrite Rinv_mult_distr.
@@ -327,16 +327,16 @@ Proof.
   discrR.
   apply H7.
   apply Rinv_neq_0_compat; discrR.
-  pattern h at 2 in |- *; replace h with (2 * (h / 2)).
+  pattern h at 2; replace h with (2 * (h / 2)).
   rewrite (cos_2a_sin (h / 2)).
-  rewrite cos_0; unfold Rsqr in |- *; ring.
-  unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
+  rewrite cos_0; unfold Rsqr; ring.
+  unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
   discrR.
-  unfold Rmin in |- *; case (Rle_dec del del_c); intro.
+  unfold Rmin; case (Rle_dec del del_c); intro.
   apply (cond_pos del).
   elim H5; intros; assumption.
   apply continuity_sin.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+  unfold Rdiv; apply Rmult_lt_0_compat;
     [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
 Qed.
 
@@ -346,10 +346,10 @@ Proof.
   intro; assert (H0 := derivable_pt_lim_sin_0).
   assert (H := derivable_pt_lim_cos_0).
   unfold derivable_pt_lim in H0, H.
-  unfold derivable_pt_lim in |- *; intros.
+  unfold derivable_pt_lim; intros.
   cut (0 < eps / 2);
     [ intro
-      | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+      | unfold Rdiv; apply Rmult_lt_0_compat;
         [ apply H1 | apply Rinv_0_lt_compat; prove_sup0 ] ].
   elim (H0 _ H2); intros alp1 H3.
   elim (H _ H2); intros alp2 H4.
@@ -364,11 +364,11 @@ Proof.
   rewrite (double_var eps); apply Rplus_lt_compat.
   apply Rle_lt_trans with (Rabs ((cos h - 1) / h)).
   rewrite Rabs_mult; rewrite Rmult_comm;
-    pattern (Rabs ((cos h - 1) / h)) at 2 in |- *; rewrite <- Rmult_1_r;
+    pattern (Rabs ((cos h - 1) / h)) at 2; rewrite <- Rmult_1_r;
       apply Rmult_le_compat_l.
   apply Rabs_pos.
   assert (H8 := SIN_bound x); elim H8; intros.
-  unfold Rabs in |- *; case (Rcase_abs (sin x)); intro.
+  unfold Rabs; case (Rcase_abs (sin x)); intro.
   rewrite <- (Ropp_involutive 1).
   apply Ropp_le_contravar; assumption.
   assumption.
@@ -378,14 +378,14 @@ Proof.
     apply H9.
   apply Rlt_le_trans with alp.
   apply H7.
-  unfold alp in |- *; apply Rmin_r.
+  unfold alp; apply Rmin_r.
   apply Rle_lt_trans with (Rabs (sin h / h - 1)).
   rewrite Rabs_mult; rewrite Rmult_comm;
-    pattern (Rabs (sin h / h - 1)) at 2 in |- *; rewrite <- Rmult_1_r;
+    pattern (Rabs (sin h / h - 1)) at 2; rewrite <- Rmult_1_r;
       apply Rmult_le_compat_l.
   apply Rabs_pos.
   assert (H8 := COS_bound x); elim H8; intros.
-  unfold Rabs in |- *; case (Rcase_abs (cos x)); intro.
+  unfold Rabs; case (Rcase_abs (cos x)); intro.
   rewrite <- (Ropp_involutive 1); apply Ropp_le_contravar; assumption.
   assumption.
   cut (Rabs h < alp1).
@@ -394,8 +394,8 @@ Proof.
     apply H9.
   apply Rlt_le_trans with alp.
   apply H7.
-  unfold alp in |- *; apply Rmin_l.
-  rewrite sin_plus; unfold Rminus, Rdiv in |- *;
+  unfold alp; apply Rmin_l.
+  rewrite sin_plus; unfold Rminus, Rdiv;
     repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
       repeat rewrite Rmult_assoc; repeat rewrite Rplus_assoc;
         apply Rplus_eq_compat_l.
@@ -404,7 +404,7 @@ Proof.
   rewrite Ropp_mult_distr_r_reverse; rewrite Ropp_mult_distr_l_reverse;
     rewrite Rmult_1_r; rewrite Rmult_1_l; rewrite Ropp_mult_distr_r_reverse;
       rewrite <- Ropp_mult_distr_l_reverse; apply Rplus_comm.
-  unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec alp1 alp2); intro.
+  unfold alp; unfold Rmin; case (Rle_dec alp1 alp2); intro.
   apply (cond_pos alp1).
   apply (cond_pos alp2).
 Qed.
@@ -419,7 +419,7 @@ Proof.
   intros; generalize (H0 _ _ _ H2 H1);
     replace (comp sin (id + fct_cte (PI / 2))%F) with
     (fun x:R => sin (x + PI / 2)); [ idtac | reflexivity ].
-  unfold derivable_pt_lim in |- *; intros.
+  unfold derivable_pt_lim; intros.
   elim (H3 eps H4); intros.
   exists x0.
   intros; rewrite <- (H (x + h)); rewrite <- (H x); apply H5; assumption.
@@ -433,26 +433,26 @@ Qed.
 
 Lemma derivable_pt_sin : forall x:R, derivable_pt sin x.
 Proof.
-  unfold derivable_pt in |- *; intro.
+  unfold derivable_pt; intro.
   exists (cos x).
   apply derivable_pt_lim_sin.
 Qed.
 
 Lemma derivable_pt_cos : forall x:R, derivable_pt cos x.
 Proof.
-  unfold derivable_pt in |- *; intro.
+  unfold derivable_pt; intro.
   exists (- sin x).
   apply derivable_pt_lim_cos.
 Qed.
 
 Lemma derivable_sin : derivable sin.
 Proof.
-  unfold derivable in |- *; intro; apply derivable_pt_sin.
+  unfold derivable; intro; apply derivable_pt_sin.
 Qed.
 
 Lemma derivable_cos : derivable cos.
 Proof.
-  unfold derivable in |- *; intro; apply derivable_pt_cos.
+  unfold derivable; intro; apply derivable_pt_cos.
 Qed.
 
 Lemma derive_pt_sin :