5 files changed, 10 insertions, 9 deletions
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 3c15a3053..b2d9c749f 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -442,7 +442,7 @@ Proof.
   apply (Rabs_pos_lt _ H0).
   ring.
   assert (H6 := Req_dec x0 (x0 + h)); elim H6; intro.
-  intro; rewrite <- H7; unfold dist, R_met; unfold R_dist;
+  intro; rewrite <- H7. unfold R_met, dist; unfold R_dist;
     unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
       apply Rabs_pos_lt.
   unfold Rdiv; apply prod_neq_R0;
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index d876b5d8e..0614f3998 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -695,7 +695,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
        exists deltatemp ; exact Htemp.
     elim (Hf_deriv eps eps_pos).
     intros deltatemp Htemp.
-     red in Hlinv ; red in Hlinv ; simpl dist in Hlinv ; unfold R_dist in Hlinv.
+     red in Hlinv ; red in Hlinv ; unfold dist in Hlinv ; unfold R_dist in Hlinv.
      assert (Hlinv' := Hlinv (fun h => (f (y+h) - f y)/h) (fun h => h <>0) l 0).
      unfold limit1_in, limit_in, dist in Hlinv' ; simpl in Hlinv'. unfold R_dist in Hlinv'.
      assert (Premisse : (forall eps : R,
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 658ffd12f..3d52a98cd 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -164,7 +164,7 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
     eps > 0 ->
     exists alp : R,
       alp > 0 /\
-      (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps).
+      (forall x:Base X, D x /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps).
 
 (*******************************)
 (** **  R is a metric space    *)
@@ -191,9 +191,9 @@ Lemma tech_limit :
 Proof.
   intros f D l x0 H H0.
   case (Rabs_pos (f x0 - l)); intros H1.
-  absurd (dist R_met (f x0) l < dist R_met (f x0) l).
+  absurd (R_met.(@dist) (f x0) l < R_met.(@dist) (f x0) l).
   apply Rlt_irrefl.
-  case (H0 (dist R_met (f x0) l)); auto.
+  case (H0 (R_met.(@dist) (f x0) l)); auto.
   intros alpha1 [H2 H3]; apply H3; auto; split; auto.
   case (dist_refl R_met x0 x0); intros Hr1 Hr2; rewrite Hr2; auto.
   case (dist_refl R_met (f x0) l); intros Hr1 Hr2; symmetry; auto.
@@ -345,8 +345,9 @@ Lemma single_limit :
     adhDa D x0 -> limit1_in f D l x0 -> limit1_in f D l' x0 -> l = l'.
 Proof.
   unfold limit1_in; unfold limit_in; intros.
+  simpl in *.
   cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps).
-  clear H0 H1; unfold dist; unfold R_met; unfold R_dist;
+  clear H0 H1; simpl @dist; unfold R_met; unfold R_dist, dist;
     unfold Rabs; case (Rcase_abs (l - l')); intros.
   cut (forall eps:R, eps > 0 -> - (l - l') < eps).
   intro; generalize (prop_eps (- (l - l')) H1); intro;
@@ -356,7 +357,7 @@ Proof.
   intros; cut (eps * / 2 > 0).
   intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
     rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
-  elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial.
+  elim (Rmult_ne eps); intros a b; rewrite b; clear a b; trivial. 
   apply (Rlt_dichotomy_converse 2 0); right; generalize Rlt_0_1; intro;
     unfold Rgt; generalize (Rplus_lt_compat_l 1 0 1 H3);
       intro; elim (Rplus_ne 1); intros a b; rewrite a in H4;
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index f05539379..7e020dd41 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -339,7 +339,7 @@ Proof.
   unfold neighbourhood in H4; elim H4; intros del H5.
   exists (pos del); split.
   apply (cond_pos del).
-  intros; unfold included in H5; apply H5; elim H6; intros; apply H8.
+  intros. unfold included in H5; apply H5; elim H6; intros; apply H8.
   unfold disc; unfold Rminus; rewrite Rplus_opp_r;
     rewrite Rabs_R0; apply H0.
   apply disc_P1.
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 5140c29c1..6ff3fa8b8 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -361,7 +361,7 @@ Proof with trivial.
   replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with
   (sum_f_R0 (fun k:nat => An k * Bn k) n +
     sum_f_R0 (fun k:nat => An k * - l) n)...
-  rewrite <- (scal_sum An n (- l)); field...
+  rewrite <- (scal_sum An n (- l)); field... 
   rewrite <- plus_sum; apply sum_eq; intros; ring...
 Qed.