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

(warn if bar is a nonprimitive projection)

4 files changed, 156 insertions, 156 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.