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

(warn if bar is a nonprimitive projection)

9 files changed, 169 insertions, 169 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 9a815d2a7e..63f907e567 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1835,36 +1835,36 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Implicit Types e : elt.
 
  Definition empty : t elt := Bst (empty_bst elt).
- Definition is_empty m : bool := Raw.is_empty m.(this).
- Definition add x e m : t elt := Bst (add_bst x e m.(is_bst)).
- Definition remove x m : t elt := Bst (remove_bst x m.(is_bst)).
- Definition mem x m : bool := Raw.mem x m.(this).
- Definition find x m : option elt := Raw.find x m.(this).
- Definition map f m : t elt' := Bst (map_bst f m.(is_bst)).
+ Definition is_empty m : bool := Raw.is_empty (this m).
+ Definition add x e m : t elt := Bst (add_bst x e (is_bst m)).
+ Definition remove x m : t elt := Bst (remove_bst x (is_bst m)).
+ Definition mem x m : bool := Raw.mem x (this m).
+ Definition find x m : option elt := Raw.find x (this m).
+ Definition map f m : t elt' := Bst (map_bst f (is_bst m)).
  Definition mapi (f:key->elt->elt') m : t elt' :=
-  Bst (mapi_bst f m.(is_bst)).
+  Bst (mapi_bst f (is_bst m)).
  Definition map2 f m (m':t elt') : t elt'' :=
-  Bst (map2_bst f m.(is_bst) m'.(is_bst)).
- Definition elements m : list (key*elt) := Raw.elements m.(this).
- Definition cardinal m := Raw.cardinal m.(this).
- Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i.
- Definition equal cmp m m' : bool := Raw.equal cmp m.(this) m'.(this).
+  Bst (map2_bst f (is_bst m) (is_bst m')).
+ Definition elements m : list (key*elt) := Raw.elements (this m).
+ Definition cardinal m := Raw.cardinal (this m).
+ Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f (this m) i.
+ Definition equal cmp m m' : bool := Raw.equal cmp (this m) (this m').
 
- Definition MapsTo x e m : Prop := Raw.MapsTo x e m.(this).
- Definition In x m : Prop := Raw.In0 x m.(this).
- Definition Empty m : Prop := Empty m.(this).
+ Definition MapsTo x e m : Prop := Raw.MapsTo x e (this m).
+ Definition In x m : Prop := Raw.In0 x (this m).
+ Definition Empty m : Prop := Empty (this m).
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
  Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
- Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@MapsTo_1 _ (this m)). Qed.
 
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
  Proof.
  unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
- apply m.(is_bst).
+ apply (is_bst m).
  Qed.
 
  Lemma mem_2 : forall m x, mem x m = true -> In x m.
@@ -1876,9 +1876,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@empty_1 elt). Qed.
 
  Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
- Proof. intros m; exact (@is_empty_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@is_empty_1 _ (this m)). Qed.
  Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
- Proof. intros m; exact (@is_empty_2 _ m.(this)). Qed.
+ Proof. intros m; exact (@is_empty_2 _ (this m)). Qed.
 
  Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
  Proof. intros m x y e; exact (@add_1 elt _ x y e). Qed.
@@ -1890,22 +1890,22 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
  Proof.
  unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.
- apply m.(is_bst).
+ apply (is_bst m).
  Qed.
  Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
- Proof. intros m x y e; exact (@remove_2 elt _ x y e m.(is_bst)). Qed.
+ Proof. intros m x y e; exact (@remove_2 elt _ x y e (is_bst m)). Qed.
  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
- Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed.
+ Proof. intros m x y e; exact (@remove_3 elt _ x y e (is_bst m)). Qed.
 
 
  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
- Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
+ Proof. intros m x e; exact (@find_1 elt _ x e (is_bst m)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
- Proof. intros m; exact (@find_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@find_2 elt (this m)). Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@fold_1 elt (this m) (is_bst m)). Qed.
 
  Lemma elements_1 : forall m x e,
    MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
@@ -1920,13 +1920,13 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Qed.
 
  Lemma elements_3 : forall m, sort lt_key (elements m).
- Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_sort elt (this m) (is_bst m)). Qed.
 
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).
- Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_nodup elt (this m) (is_bst m)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
- Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.
+ Proof. intro m; exact (@elements_cardinal elt (this m)). Qed.
 
  Definition Equal m m' := forall y, find y m = find y m'.
  Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
@@ -1962,7 +1962,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
         MapsTo x e m -> MapsTo x (f e) (map f m).
- Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f (this m) x e). Qed.
 
  Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
  Proof.
@@ -1973,7 +1973,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
         (f:key->elt->elt'), MapsTo x e m ->
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f (this m) x e). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
  Proof.
@@ -1987,8 +1987,8 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof.
  unfold find, map2, In; intros elt elt' elt'' m m' x f.
  do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
- apply m.(is_bst).
- apply m'.(is_bst).
+ apply (is_bst m).
+ apply (is_bst m').
  Qed.
 
  Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
@@ -1997,8 +1997,8 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof.
  unfold In, map2; intros elt elt' elt'' m m' x f.
  do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
- apply m.(is_bst).
- apply m'.(is_bst).
+ apply (is_bst m).
+ apply (is_bst m').
  Qed.
 
 End IntMake.
@@ -2124,7 +2124,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   (* Proofs about [eq] and [lt] *)
 
   Definition selements (m1 : t) :=
-   LO.MapS.Build_slist (P.elements_sort m1.(is_bst)).
+   LO.MapS.Build_slist (P.elements_sort (is_bst m1)).
 
   Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
   Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 7bc9edff8d..b23885154b 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -466,39 +466,39 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Implicit Types e : elt.
 
  Definition empty : t elt := Bbst (empty_bst elt) (empty_avl elt).
- Definition is_empty m : bool := is_empty m.(this).
+ Definition is_empty m : bool := is_empty (this m).
  Definition add x e m : t elt :=
-  Bbst (add_bst x e m.(is_bst)) (add_avl x e m.(is_avl)).
+  Bbst (add_bst x e (is_bst m)) (add_avl x e (is_avl m)).
  Definition remove x m : t elt :=
-  Bbst (remove_bst x m.(is_bst)) (remove_avl x m.(is_avl)).
- Definition mem x m : bool := mem x m.(this).
- Definition find x m : option elt := find x m.(this).
+  Bbst (remove_bst x (is_bst m)) (remove_avl x (is_avl m)).
+ Definition mem x m : bool := mem x (this m).
+ Definition find x m : option elt := find x (this m).
  Definition map f m : t elt' :=
-  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
+  Bbst (map_bst f (is_bst m)) (map_avl f (is_avl m)).
  Definition mapi (f:key->elt->elt') m : t elt' :=
-  Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)).
+  Bbst (mapi_bst f (is_bst m)) (mapi_avl f (is_avl m)).
  Definition map2 f m (m':t elt') : t elt'' :=
-  Bbst (map2_bst f m.(is_bst) m'.(is_bst)) (map2_avl f m.(is_avl) m'.(is_avl)).
- Definition elements m : list (key*elt) := elements m.(this).
- Definition cardinal m := cardinal m.(this).
- Definition fold (A:Type) (f:key->elt->A->A) m i := fold (A:=A) f m.(this) i.
- Definition equal cmp m m' : bool := equal cmp m.(this) m'.(this).
+  Bbst (map2_bst f (is_bst m) (is_bst m')) (map2_avl f (is_avl m) (is_avl m')).
+ Definition elements m : list (key*elt) := elements (this m).
+ Definition cardinal m := cardinal (this m).
+ Definition fold (A:Type) (f:key->elt->A->A) m i := fold (A:=A) f (this m) i.
+ Definition equal cmp m m' : bool := equal cmp (this m) (this m').
 
- Definition MapsTo x e m : Prop := MapsTo x e m.(this).
- Definition In x m : Prop := In0 x m.(this).
- Definition Empty m : Prop := Empty m.(this).
+ Definition MapsTo x e m : Prop := MapsTo x e (this m).
+ Definition In x m : Prop := In0 x (this m).
+ Definition Empty m : Prop := Empty (this m).
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
  Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
- Proof. intros m; exact (@MapsTo_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@MapsTo_1 _ (this m)). Qed.
 
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
  Proof.
  unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.
- apply m.(is_bst).
+ apply (is_bst m).
  Qed.
 
  Lemma mem_2 : forall m x, mem x m = true -> In x m.
@@ -510,9 +510,9 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof. exact (@empty_1 elt). Qed.
 
  Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
- Proof. intros m; exact (@is_empty_1 _ m.(this)). Qed.
+ Proof. intros m; exact (@is_empty_1 _ (this m)). Qed.
  Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
- Proof. intros m; exact (@is_empty_2 _ m.(this)). Qed.
+ Proof. intros m; exact (@is_empty_2 _ (this m)). Qed.
 
  Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
  Proof. intros m x y e; exact (@add_1 elt _ x y e). Qed.
@@ -524,22 +524,22 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
  Proof.
  unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.
- apply m.(is_bst).
+ apply (is_bst m).
  Qed.
  Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
- Proof. intros m x y e; exact (@remove_2 elt _ x y e m.(is_bst)). Qed.
+ Proof. intros m x y e; exact (@remove_2 elt _ x y e (is_bst m)). Qed.
  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
- Proof. intros m x y e; exact (@remove_3 elt _ x y e m.(is_bst)). Qed.
+ Proof. intros m x y e; exact (@remove_3 elt _ x y e (is_bst m)). Qed.
 
 
  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
- Proof. intros m x e; exact (@find_1 elt _ x e m.(is_bst)). Qed.
+ Proof. intros m x e; exact (@find_1 elt _ x e (is_bst m)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
- Proof. intros m; exact (@find_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@find_2 elt (this m)). Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- Proof. intros m; exact (@fold_1 elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@fold_1 elt (this m) (is_bst m)). Qed.
 
  Lemma elements_1 : forall m x e,
    MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
@@ -554,13 +554,13 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Qed.
 
  Lemma elements_3 : forall m, sort lt_key (elements m).
- Proof. intros m; exact (@elements_sort elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_sort elt (this m) (is_bst m)). Qed.
 
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).
- Proof. intros m; exact (@elements_nodup elt m.(this) m.(is_bst)). Qed.
+ Proof. intros m; exact (@elements_nodup elt (this m) (is_bst m)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
- Proof. intro m; exact (@elements_cardinal elt m.(this)). Qed.
+ Proof. intro m; exact (@elements_cardinal elt (this m)). Qed.
 
  Definition Equal m m' := forall y, find y m = find y m'.
  Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
@@ -596,7 +596,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
 
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
         MapsTo x e m -> MapsTo x (f e) (map f m).
- Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@map_1 elt elt' f (this m) x e). Qed.
 
  Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
  Proof.
@@ -607,7 +607,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
         (f:key->elt->elt'), MapsTo x e m ->
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f m.(this) x e). Qed.
+ Proof. intros elt elt' m x e f; exact (@mapi_1 elt elt' f (this m) x e). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
  Proof.
@@ -621,8 +621,8 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof.
  unfold find, map2, In; intros elt elt' elt'' m m' x f.
  do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.
- apply m.(is_bst).
- apply m'.(is_bst).
+ apply (is_bst m).
+ apply (is_bst m').
  Qed.
 
  Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
@@ -631,8 +631,8 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Proof.
  unfold In, map2; intros elt elt' elt'' m m' x f.
  do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.
- apply m.(is_bst).
- apply m'.(is_bst).
+ apply (is_bst m).
+ apply (is_bst m').
  Qed.
 
 End IntMake.
@@ -655,7 +655,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    match D.compare e e' with EQ _ => true | _ => false end.
 
   Definition elements (m:t) :=
-    LO.MapS.Build_slist (Raw.Proofs.elements_sort m.(is_bst)).
+    LO.MapS.Build_slist (Raw.Proofs.elements_sort (is_bst m)).
 
   (** * As comparison function, we propose here a non-structural
     version faithful to the code of Ocaml's Map library, instead of
@@ -750,7 +750,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   (* Proofs about [eq] and [lt] *)
 
   Definition selements (m1 : t) :=
-   LO.MapS.Build_slist (elements_sort m1.(is_bst)).
+   LO.MapS.Build_slist (elements_sort (is_bst m1)).
 
   Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
   Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 4febd64842..335fdc3232 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -1037,106 +1037,106 @@ Section Elt.
  Implicit Types e : elt.
 
  Definition empty : t elt := Build_slist (Raw.empty_sorted elt).
- Definition is_empty m : bool := Raw.is_empty m.(this).
- Definition add x e m : t elt := Build_slist (Raw.add_sorted m.(sorted) x e).
- Definition find x m : option elt := Raw.find x m.(this).
- Definition remove x m : t elt := Build_slist (Raw.remove_sorted m.(sorted) x).
- Definition mem x m : bool := Raw.mem x m.(this).
- Definition map f m : t elt' := Build_slist (Raw.map_sorted m.(sorted) f).
- Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_sorted m.(sorted) f).
+ Definition is_empty m : bool := Raw.is_empty (this m).
+ Definition add x e m : t elt := Build_slist (Raw.add_sorted (sorted m) x e).
+ Definition find x m : option elt := Raw.find x (this m).
+ Definition remove x m : t elt := Build_slist (Raw.remove_sorted (sorted m) x).
+ Definition mem x m : bool := Raw.mem x (this m).
+ Definition map f m : t elt' := Build_slist (Raw.map_sorted (sorted m) f).
+ Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_sorted (sorted m) f).
  Definition map2 f m (m':t elt') : t elt'' :=
-   Build_slist (Raw.map2_sorted f m.(sorted) m'.(sorted)).
- Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
- Definition cardinal m := length m.(this).
- Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
- Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
+   Build_slist (Raw.map2_sorted f (sorted m) (sorted m')).
+ Definition elements m : list (key*elt) := @Raw.elements elt (this m).
+ Definition cardinal m := length (this m).
+ Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f (this m) i.
+ Definition equal cmp m m' : bool := @Raw.equal elt cmp (this m) (this m').
 
- Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
- Definition In x m : Prop := Raw.PX.In x m.(this).
- Definition Empty m : Prop := Raw.Empty m.(this).
+ Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e (this m).
+ Definition In x m : Prop := Raw.PX.In x (this m).
+ Definition Empty m : Prop := Raw.Empty (this m).
 
  Definition Equal m m' := forall y, find y m = find y m'.
  Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
          (forall k, In k m <-> In k m') /\
          (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
- Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp m.(this) m'.(this).
+ Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp (this m) (this m').
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt.
  Definition lt_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.ltk elt.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
- Proof. intros m; exact (@Raw.PX.MapsTo_eq elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.PX.MapsTo_eq elt (this m)). Qed.
 
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
- Proof. intros m; exact (@Raw.mem_1 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.mem_1 elt (this m) (sorted m)). Qed.
  Lemma mem_2 : forall m x, mem x m = true -> In x m.
- Proof. intros m; exact (@Raw.mem_2 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.mem_2 elt (this m) (sorted m)). Qed.
 
  Lemma empty_1 : Empty empty.
  Proof. exact (@Raw.empty_1 elt). Qed.
 
  Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
- Proof. intros m; exact (@Raw.is_empty_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.is_empty_1 elt (this m)). Qed.
  Lemma is_empty_2 :  forall m, is_empty m = true -> Empty m.
- Proof. intros m; exact (@Raw.is_empty_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.is_empty_2 elt (this m)). Qed.
 
  Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
- Proof. intros m; exact (@Raw.add_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_1 elt (this m)). Qed.
  Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
- Proof. intros m; exact (@Raw.add_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_2 elt (this m)). Qed.
  Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
- Proof. intros m; exact (@Raw.add_3 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_3 elt (this m)). Qed.
 
  Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
- Proof. intros m; exact (@Raw.remove_1 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.remove_1 elt (this m) (sorted m)). Qed.
  Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
- Proof. intros m; exact (@Raw.remove_2 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.remove_2 elt (this m) (sorted m)). Qed.
  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
- Proof. intros m; exact (@Raw.remove_3 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.remove_3 elt (this m) (sorted m)). Qed.
 
  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
- Proof. intros m; exact (@Raw.find_1 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.find_1 elt (this m) (sorted m)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
- Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.find_2 elt (this m)). Qed.
 
  Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
- Proof. intros m; exact (@Raw.elements_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.elements_1 elt (this m)). Qed.
  Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
- Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.elements_2 elt (this m)). Qed.
  Lemma elements_3 : forall m, sort lt_key (elements m).
- Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.elements_3 elt (this m) (sorted m)). Qed.
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).
- Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(sorted)). Qed.
+ Proof. intros m; exact (@Raw.elements_3w elt (this m) (sorted m)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
  Proof. intros; reflexivity. Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.fold_1 elt (this m)). Qed.
 
  Lemma equal_1 : forall m m' cmp, Equivb cmp m m' -> equal cmp m m' = true.
- Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed.
+ Proof. intros m m'; exact (@Raw.equal_1 elt (this m) (sorted m) (this m') (sorted m')). Qed.
  Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'.
- Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(sorted) m'.(this) m'.(sorted)). Qed.
+ Proof. intros m m'; exact (@Raw.equal_2 elt (this m) (sorted m) (this m') (sorted m')). Qed.
 
  End Elt.
 
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
         MapsTo x e m -> MapsTo x (f e) (map f m).
- Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' (this m)). Qed.
  Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'),
         In x (map f m) -> In x m.
- Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' (this m)). Qed.
 
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
         (f:key->elt->elt'), MapsTo x e m ->
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' (this m)). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
- Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' (this m)). Qed.
 
  Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 	(x:key)(f:option elt->option elt'->option elt''),
@@ -1144,14 +1144,14 @@ Section Elt.
         find x (map2 f m m') = f (find x m) (find x m').
  Proof.
  intros elt elt' elt'' m m' x f;
- exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x).
+ exact (@Raw.map2_1 elt elt' elt'' f (this m) (sorted m) (this m') (sorted m') x).
  Qed.
  Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 	(x:key)(f:option elt->option elt'->option elt''),
         In x (map2 f m m') -> In x m \/ In x m'.
  Proof.
  intros elt elt' elt'' m m' x f;
- exact (@Raw.map2_2 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x).
+ exact (@Raw.map2_2 elt elt' elt'' f (this m) (sorted m) (this m') (sorted m') x).
  Qed.
 
 End Make.
@@ -1182,7 +1182,7 @@ Fixpoint eq_list (m m' : list (X.t * D.t)) : Prop :=
    | _, _ => False
   end.
 
-Definition eq m m' := eq_list m.(this) m'.(this).
+Definition eq m m' := eq_list (this m) (this m').
 
 Fixpoint lt_list (m m' : list (X.t * D.t)) : Prop :=
   match m, m' with
@@ -1197,7 +1197,7 @@ Fixpoint lt_list (m m' : list (X.t * D.t)) : Prop :=
       end
   end.
 
-Definition lt m m' := lt_list m.(this) m'.(this).
+Definition lt m m' := lt_list (this m) (this m').
 
 Lemma eq_equal : forall m m', eq m m' <-> equal cmp m m' = true.
 Proof.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index a923f4e6f9..12550ddf9a 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -882,102 +882,102 @@ Section Elt.
  Implicit Types e : elt.
 
  Definition empty : t elt := Build_slist (Raw.empty_NoDup elt).
- Definition is_empty m : bool := Raw.is_empty m.(this).
- Definition add x e m : t elt := Build_slist (Raw.add_NoDup m.(NoDup) x e).
- Definition find x m : option elt := Raw.find x m.(this).
- Definition remove x m : t elt := Build_slist (Raw.remove_NoDup m.(NoDup) x).
- Definition mem x m : bool := Raw.mem x m.(this).
- Definition map f m : t elt' := Build_slist (Raw.map_NoDup m.(NoDup) f).
- Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_NoDup m.(NoDup) f).
+ Definition is_empty m : bool := Raw.is_empty (this m).
+ Definition add x e m : t elt := Build_slist (Raw.add_NoDup (NoDup m) x e).
+ Definition find x m : option elt := Raw.find x (this m).
+ Definition remove x m : t elt := Build_slist (Raw.remove_NoDup (NoDup m) x).
+ Definition mem x m : bool := Raw.mem x (this m).
+ Definition map f m : t elt' := Build_slist (Raw.map_NoDup (NoDup m) f).
+ Definition mapi (f:key->elt->elt') m : t elt' := Build_slist (Raw.mapi_NoDup (NoDup m) f).
  Definition map2 f m (m':t elt') : t elt'' :=
-   Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)).
- Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
- Definition cardinal m := length m.(this).
- Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
- Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
- Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
- Definition In x m : Prop := Raw.PX.In x m.(this).
- Definition Empty m : Prop := Raw.Empty m.(this).
+   Build_slist (Raw.map2_NoDup f (NoDup m) (NoDup m')).
+ Definition elements m : list (key*elt) := @Raw.elements elt (this m).
+ Definition cardinal m := length (this m).
+ Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f (this m) i.
+ Definition equal cmp m m' : bool := @Raw.equal elt cmp (this m) (this m').
+ Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e (this m).
+ Definition In x m : Prop := Raw.PX.In x (this m).
+ Definition Empty m : Prop := Raw.Empty (this m).
 
  Definition Equal m m' := forall y, find y m = find y m'.
  Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
          (forall k, In k m <-> In k m') /\
          (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
- Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp m.(this) m'.(this).
+ Definition Equivb cmp m m' : Prop := @Raw.Equivb elt cmp (this m) (this m').
 
  Definition eq_key : (key*elt) -> (key*elt) -> Prop := @Raw.PX.eqk elt.
  Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop:= @Raw.PX.eqke elt.
 
  Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.
- Proof. intros m; exact (@Raw.PX.MapsTo_eq elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.PX.MapsTo_eq elt (this m)). Qed.
 
  Lemma mem_1 : forall m x, In x m -> mem x m = true.
- Proof. intros m; exact (@Raw.mem_1 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.mem_1 elt (this m) (NoDup m)). Qed.
  Lemma mem_2 : forall m x, mem x m = true -> In x m.
- Proof. intros m; exact (@Raw.mem_2 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.mem_2 elt (this m) (NoDup m)). Qed.
 
  Lemma empty_1 : Empty empty.
  Proof. exact (@Raw.empty_1 elt). Qed.
 
  Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
- Proof. intros m; exact (@Raw.is_empty_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.is_empty_1 elt (this m)). Qed.
  Lemma is_empty_2 :  forall m, is_empty m = true -> Empty m.
- Proof. intros m; exact (@Raw.is_empty_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.is_empty_2 elt (this m)). Qed.
 
  Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
- Proof. intros m; exact (@Raw.add_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_1 elt (this m)). Qed.
  Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
- Proof. intros m; exact (@Raw.add_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_2 elt (this m)). Qed.
  Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
- Proof. intros m; exact (@Raw.add_3 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.add_3 elt (this m)). Qed.
 
  Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
- Proof. intros m; exact (@Raw.remove_1 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.remove_1 elt (this m) (NoDup m)). Qed.
  Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
- Proof. intros m; exact (@Raw.remove_2 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.remove_2 elt (this m) (NoDup m)). Qed.
  Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
- Proof. intros m; exact (@Raw.remove_3 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.remove_3 elt (this m) (NoDup m)). Qed.
 
  Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
- Proof. intros m; exact (@Raw.find_1 elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.find_1 elt (this m) (NoDup m)). Qed.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
- Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.find_2 elt (this m)). Qed.
 
  Lemma elements_1 : forall m x e, MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
- Proof. intros m; exact (@Raw.elements_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.elements_1 elt (this m)). Qed.
  Lemma elements_2 : forall m x e, InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
- Proof. intros m; exact (@Raw.elements_2 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.elements_2 elt (this m)). Qed.
  Lemma elements_3w : forall m, NoDupA eq_key (elements m).
- Proof. intros m; exact (@Raw.elements_3w elt m.(this) m.(NoDup)). Qed.
+ Proof. intros m; exact (@Raw.elements_3w elt (this m) (NoDup m)). Qed.
 
  Lemma cardinal_1 : forall m, cardinal m = length (elements m).
  Proof. intros; reflexivity. Qed.
 
  Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
- Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
+ Proof. intros m; exact (@Raw.fold_1 elt (this m)). Qed.
 
  Lemma equal_1 : forall m m' cmp, Equivb cmp m m' -> equal cmp m m' = true.
- Proof. intros m m'; exact (@Raw.equal_1 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed.
+ Proof. intros m m'; exact (@Raw.equal_1 elt (this m) (NoDup m) (this m') (NoDup m')). Qed.
  Lemma equal_2 : forall m m' cmp, equal cmp m m' = true -> Equivb cmp m m'.
- Proof. intros m m'; exact (@Raw.equal_2 elt m.(this) m.(NoDup) m'.(this) m'.(NoDup)). Qed.
+ Proof. intros m m'; exact (@Raw.equal_2 elt (this m) (NoDup m) (this m') (NoDup m')). Qed.
 
  End Elt.
 
  Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
         MapsTo x e m -> MapsTo x (f e) (map f m).
- Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' (this m)). Qed.
  Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'),
         In x (map f m) -> In x m.
- Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' (this m)). Qed.
 
  Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
         (f:key->elt->elt'), MapsTo x e m ->
         exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).
- Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' (this m)). Qed.
  Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
- Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed.
+ Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' (this m)). Qed.
 
  Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 	(x:key)(f:option elt->option elt'->option elt''),
@@ -985,14 +985,14 @@ Section Elt.
         find x (map2 f m m') = f (find x m) (find x m').
  Proof.
  intros elt elt' elt'' m m' x f;
- exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x).
+ exact (@Raw.map2_1 elt elt' elt'' f (this m) (NoDup m) (this m') (NoDup m') x).
  Qed.
  Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
 	(x:key)(f:option elt->option elt'->option elt''),
         In x (map2 f m m') -> In x m \/ In x m'.
  Proof.
  intros elt elt' elt'' m m' x f;
- exact (@Raw.map2_2 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x).
+ exact (@Raw.map2_2 elt elt' elt'' f (this m) (NoDup m) (this m') (NoDup m') x).
  Qed.
 
 End Make.
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 86894cd1f2..4576ff4cbe 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -74,8 +74,8 @@ Record retract_cond : Prop :=
 
 (** The dependent elimination above implies the axiom of choice: *)
 
-Lemma AC : forall r:retract_cond, retract -> forall a:A, r.(j2) (r.(i2) a) = a.
-Proof. intros r. exact r.(inv2). Qed.
+Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
+Proof. intros r. exact (inv2 r). Qed.
 
 End Retracts.
 
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 0ba2799bfb..6a18f59fc4 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -445,7 +445,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.
  Arguments Mkt this {is_ok}.
  Hint Resolve is_ok : typeclass_instances.
 
- Definition In (x : elt)(s : t) := M.In x s.(this).
+ Definition In (x : elt)(s : t) := M.In x (this s).
  Definition Equal (s s' : t) := forall a : elt, In a s <-> In a s'.
  Definition Subset (s s' : t) := forall a : elt, In a s -> In a s'.
  Definition Empty (s : t) := forall a : elt, ~ In a s.
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.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 346c300ee5..4591c7ed94 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -128,9 +128,9 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
       [EqualityType] and [DecidableType] *)
 
 Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). 
- Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _).
- Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _).
+ Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
+ Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
+ Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.