Error when [foo.(bar)] is used with nonprojection [bar]

(warn if bar is a nonprimitive projection)

2 files changed, 7 insertions, 7 deletions

diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index e66130b347..d16b5a3020 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -82,7 +82,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
  elim (Hyp eps eps_pos) ; intros delta Hyp2.
  assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0).
   clear-a lb ub a_encad delta.
-  apply Rmin_pos ; [exact (delta.(cond_pos)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
+  apply Rmin_pos ; [exact ((cond_pos delta)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
  exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond).
  intros h h_neq h_encad.
  replace (g (a + h) - g a) with (f (a + h) - f a).
@@ -120,7 +120,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
  elim (Hyp eps eps_pos) ; intros delta Hyp2.
  assert (Pos_cond : Rmin delta (Rmin (ub - a) (a - lb)) > 0).
   clear-a lb ub a_encad delta.
-  apply Rmin_pos ; [exact (delta.(cond_pos)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
+  apply Rmin_pos ; [exact ((cond_pos delta)) | apply Rmin_pos ] ; apply Rlt_Rminus ; intuition.
  exists (mkposreal (Rmin delta (Rmin (ub - a) (a - lb))) Pos_cond).
  intros h h_neq h_encad.
  replace (f (a + h) - f a) with (g (a + h) - g a).
@@ -696,7 +696,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
        intros deltatemp' Htemp'.
         exists deltatemp'.
         split.
-         exact deltatemp'.(cond_pos).
+         exact (cond_pos deltatemp').
          intros htemp cond.
           apply (Htemp' htemp).
           exact (proj1 cond).
@@ -721,7 +721,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq.
        assert (mydelta_pos : mydelta > 0).
         unfold mydelta, Rmin.
         case (Rle_dec delta alpha).
-        intro ; exact (delta.(cond_pos)).
+        intro ; exact ((cond_pos delta)).
         intro ; exact alpha_pos.
        elim (g_cont mydelta mydelta_pos).
        intros delta' new_g_cont.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index b6b72de889..2bfd99ebc7 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -136,7 +136,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 /\ X.(dist) x x0 < alp -> X'.(dist) (f x) l < eps).
+      (forall x:Base X, D x /\ (dist X) x x0 < alp -> (dist X') (f x) l < eps).
 
 (*******************************)
 (** **  R is a metric space    *)
@@ -165,9 +165,9 @@ Lemma tech_limit :
 Proof.
   intros f D l x0 H H0.
   case (Rabs_pos (f x0 - l)); intros H1.
-  absurd (R_met.(@dist) (f x0) l < R_met.(@dist) (f x0) l).
+  absurd ((@dist R_met) (f x0) l < (@dist R_met) (f x0) l).
   apply Rlt_irrefl.
-  case (H0 (R_met.(@dist) (f x0) l)); auto.
+  case (H0 ((@dist R_met) (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.