Merge PR #8829: Error when [foo.(bar)] is used with nonprojection [bar], warn if [bar] nonprimitive projection.

Reviewed-by: ppedrot

24 files changed, 371 insertions, 331 deletions

diff --git a/CHANGES.md b/CHANGES.md
index bf4244bdf9..f17e775853 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -46,6 +46,11 @@ Specification language, type inference
   solved by writing an explicit `return` clause, sometimes even simply
   an explicit `return _` clause.
 
+- Using non-projection values with the projection syntax is not
+  allowed. For instance "0.(S)" is not a valid way to write "S 0".
+  Projections from non-primitive (emulated) records are allowed with
+  warning "nonprimitive-projection-syntax".
+
 Kernel
 
 - Added primitive integers
diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh
new file mode 100644
index 0000000000..c04621114f
--- /dev/null
+++ b/dev/ci/user-overlays/08829-proj-syntax-check.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then
+    lambdaRust_CI_REF=proj-syntax-check
+    lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust
+    lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive
+fi
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 349402035c..7a3e9881ea 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1033,7 +1033,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
   | TrueGlobal (VarRef _) when no_secvar ->
       (* Rule out section vars since these should have been found by intern_var *)
       raise Not_found
-  | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
+  | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
       let nids = List.length ids in
@@ -1043,7 +1043,6 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       let terms = make_subst ids (List.map fst args1) in
       let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
       let infos = (Id.Map.empty, env) in
-      let projapp = match c with NRef _ -> true | _ -> false in
       let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
       let loc = c.loc in
       let err () =
@@ -1067,33 +1066,60 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
         user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
       | Some _, _ -> err ()
       in
-      c, projapp, args2
+      c, None, args2
+
+let warn_nonprimitive_projection =
+  CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled
+    Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
+
+let error_nonprojection_syntax ?loc qid =
+  CErrors.user_err ?loc ~hdr:"nonprojection-syntax" Pp.(pr_qualid qid ++ str" is not a projection.")
+
+let check_applied_projection isproj realref qid =
+  match isproj with
+  | None -> ()
+  | Some projargs ->
+    let is_prim = match realref with
+      | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false
+      | Some (ConstRef c) ->
+        if Recordops.is_primitive_projection c then true
+        else if Recordops.is_projection c then false
+        else error_nonprojection_syntax ?loc:qid.loc qid
+        (* TODO check projargs, note we will need implicit argument info *)
+    in
+    if not is_prim then warn_nonprimitive_projection ?loc:qid.loc qid
 
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid =
+let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid =
   let loc = qid.CAst.loc in
   if qualid_is_ident qid then
-      try intern_var env lvar namedctx loc (qualid_basename qid) us, args
+      try
+        let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
+        check_applied_projection isproj None qid;
+        res, args
       with Not_found ->
       try
-        let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
+        let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
+        check_applied_projection isproj realref qid;
 	let x, imp, scopes, l = find_appl_head_data r in
 	  (x,imp,scopes,l), args2
       with Not_found ->
         (* Extra allowance for non globalizing functions *)
         if !interning_grammar || env.unb then
+          (* check_applied_projection ?? *)
           (gvar (loc,qualid_basename qid) us, [], [], []), args
         else Nametab.error_global_not_found qid
   else
-    let r,projapp,args2 =
+    let r,realref,args2 =
       try intern_qualid qid intern env ntnvars us args
       with Not_found -> Nametab.error_global_not_found qid
     in
+    check_applied_projection isproj realref qid;
     let x, imp, scopes, l = find_appl_head_data r in
     (x,imp,scopes,l), args2
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
-    intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None)
+    intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env}
       Environ.empty_named_context_val
@@ -1827,8 +1853,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
   let rec intern env = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
-          intern_applied_reference intern env (Environ.named_context_val globalenv)
-	    lvar us [] ref
+          intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
+            lvar us [] ref
 	in
 	  apply_impargs c env imp subscopes l loc
 
@@ -1933,30 +1959,31 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
-          intern_applied_reference intern env (Environ.named_context_val globalenv)
-	    lvar us args ref 
+          intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
+            lvar us args ref
 	in
         (* Rem: GApp(_,f,[]) stands for @f *)
         if args = [] then DAst.make ?loc @@ GApp (f,[]) else
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
-        let f,args = match f.CAst.v with
+        let isproj,f,args = match f.CAst.v with
           (* Compact notations like "t.(f args') args" *)
-          | CApp ((Some _,f), args') when not (Option.has_some isproj) ->
-	    f,args'@args
+          | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
+            isproj',f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
-          | _ -> f,args in
+          | _ -> isproj,f,args in
 	let (c,impargs,args_scopes,l),args =
           match f.CAst.v with
             | CRef (ref,us) -> 
-	       intern_applied_reference intern env
+               intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
             | CNotation (ntn,([],[],[],[])) ->
+                assert (Option.is_empty isproj);
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
-            | _ -> (intern env f,[],[],[]), args in
+            | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in
           apply_impargs c env impargs args_scopes
 	    (merge_impargs l args) loc
 
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index eb84b1203d..36ed0210e3 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -594,7 +594,7 @@ Qed.
  Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
  Proof.
   rewrite Pos.add_comm.
-  apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
+  apply (pow_pos_add Rsth (Rmul_ext Reqe) (ARmul_assoc ARth)).
  Qed.
 
  Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
@@ -1085,7 +1085,7 @@ Section POWER.
    - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
    - simpl. rewrite IHpe. Esimpl.
    - simpl. rewrite Ppow_N_ok by reflexivity.
-     rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl.
+     rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl.
      induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
   Qed.
 
diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 62505453f9..e0e2232be5 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -87,40 +87,40 @@ Notation "x < y" := (rlt x y).
 
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+  reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+  symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+  transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
 as sor_setoid.
 
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
 Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
 Qed.
 Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
 Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
 Qed.
 Add Morphism ropp with signature req ==> req as ropp_morph.
 Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
 Qed.
 Add Morphism rle with signature req ==> req ==> iff as rle_morph.
 Proof.
-exact sor.(SORle_wd).
+exact (SORle_wd sor).
 Qed.
 Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
 Proof.
-exact sor.(SORlt_wd).
+exact (SORlt_wd sor).
 Qed.
 
-Add Ring SOR : sor.(SORrt).
+Add Ring SOR : (SORrt sor).
 
 Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
 Proof.
 intros x1 x2 H1 y1 y2 H2.
-rewrite (sor.(SORrt).(Rsub_def) x1 y1).
-rewrite (sor.(SORrt).(Rsub_def) x2 y2).
+rewrite ((Rsub_def (SORrt sor)) x1 y1).
+rewrite ((Rsub_def (SORrt sor)) x2 y2).
 rewrite H1; now rewrite H2.
 Qed.
 
@@ -180,22 +180,22 @@ Qed.
 (* Relations *)
 
 Theorem Rle_refl : forall n : R, n <= n.
-Proof sor.(SORle_refl).
+Proof (SORle_refl sor).
 
 Theorem Rle_antisymm : forall n m : R, n <= m -> m <= n -> n == m.
-Proof sor.(SORle_antisymm).
+Proof (SORle_antisymm sor).
 
 Theorem Rle_trans : forall n m p : R, n <= m -> m <= p -> n <= p.
-Proof sor.(SORle_trans).
+Proof (SORle_trans sor).
 
 Theorem Rlt_trichotomy : forall n m : R,  n < m \/ n == m \/ m < n.
-Proof sor.(SORlt_trichotomy).
+Proof (SORlt_trichotomy sor).
 
 Theorem Rlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m.
-Proof sor.(SORlt_le_neq).
+Proof (SORlt_le_neq sor).
 
 Theorem Rneq_0_1 : 0 ~= 1.
-Proof sor.(SORneq_0_1).
+Proof (SORneq_0_1 sor).
 
 Theorem Req_em : forall n m : R, n == m \/ n ~= m.
 Proof.
@@ -274,8 +274,8 @@ Qed.
 Theorem Rplus_le_mono_l : forall n m p : R, n <= m <-> p + n <= p + m.
 Proof.
 intros n m p; split.
-apply sor.(SORplus_le_mono_l).
-intro H. apply (sor.(SORplus_le_mono_l) (p + n) (p + m) (- p)) in H.
+apply (SORplus_le_mono_l sor).
+intro H. apply ((SORplus_le_mono_l sor) (p + n) (p + m) (- p)) in H.
 setoid_replace (- p + (p + n)) with n in H by ring.
 setoid_replace (- p + (p + m)) with m in H by ring. assumption.
 Qed.
@@ -375,7 +375,7 @@ Qed.
 (* Times and order *)
 
 Theorem Rtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m.
-Proof sor.(SORtimes_pos_pos).
+Proof (SORtimes_pos_pos sor).
 
 Theorem Rtimes_nonneg_nonneg : forall n m : R, 0 <= n -> 0 <= m -> 0 <= n * m.
 Proof.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 782fab5e68..9504f4edf6 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -81,30 +81,30 @@ Record SORaddon := mk_SOR_addon {
 Variable addon : SORaddon.
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+  reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+  symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+  transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
 as micomega_sor_setoid.
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
 Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
 Qed.
 Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
 Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
 Qed.
 Add Morphism ropp with signature req ==> req as ropp_morph.
 Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
 Qed.
 Add Morphism rle with signature req ==> req ==> iff as rle_morph.
 Proof.
-  exact sor.(SORle_wd).
+  exact (SORle_wd sor).
 Qed.
 Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
 Proof.
-  exact sor.(SORlt_wd).
+  exact (SORlt_wd sor).
 Qed.
 
 Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
@@ -124,12 +124,12 @@ Ltac le_elim H := rewrite (Rle_lt_eq sor) in H; destruct H as [H | H].
 
 Lemma cleb_sound : forall x y : C, x [<=] y = true -> [x] <= [y].
 Proof.
-  exact addon.(SORcleb_morph).
+  exact (SORcleb_morph addon).
 Qed.
 
 Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
 Proof.
-intros x y H1. apply addon.(SORcneqb_morph). unfold cneqb, negb in H1.
+intros x y H1. apply (SORcneqb_morph addon). unfold cneqb, negb in H1.
 destruct (ceqb x y); now try discriminate.
 Qed.
 
@@ -325,9 +325,9 @@ Definition map_option2 (A B C : Type) (f : A -> B -> option C)
 Arguments map_option2 [A B C] f o o'.
 
 Definition Rops_wd := mk_reqe (*rplus rtimes ropp req*)
-                       sor.(SORplus_wd)
-                       sor.(SORtimes_wd)
-                       sor.(SORopp_wd).
+                       (SORplus_wd sor)
+                       (SORtimes_wd sor)
+                       (SORopp_wd sor).
 
 Definition pexpr_times_nformula (e: PolC) (f : NFormula) : option NFormula :=
   let (ef,o) := f in
@@ -368,8 +368,8 @@ Proof.
   destruct f.
   intros. destruct o ; inversion H0 ; try discriminate.
   simpl in *.    unfold eval_pol in *.
-  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm)).
+  rewrite (Pmul_ok (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))  (SORrm addon)).
   rewrite H. apply (Rtimes_0_r sor).
 Qed.
 
@@ -385,8 +385,8 @@ Proof.
   intros. inversion H2 ; simpl.
   unfold eval_pol.
   destruct o1; simpl;
-  rewrite (Pmul_ok sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
+  rewrite (Pmul_ok (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))  (SORrm addon));
   apply OpMult_sound with (3:= H);assumption.
 Qed.
 
@@ -402,8 +402,8 @@ Proof.
   intros. inversion H2 ; simpl.
   unfold eval_pol.
   destruct o1; simpl;
-  rewrite (Padd_ok sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
+  rewrite (Padd_ok (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))  (SORrm addon));
   apply OpAdd_sound with (3:= H);assumption.
 Qed.
 
@@ -422,12 +422,12 @@ Proof.
   (* index is out-of-bounds *)
   inversion H0.
   rewrite Heq. simpl.
-  now apply  addon.(SORrm).(morph0).
+  now apply  (morph0 (SORrm addon)).
   (* PsatzSquare *)
   simpl. intros. inversion H0.
   simpl. unfold eval_pol.
-  rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
+  rewrite (Psquare_ok (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))  (SORrm addon));
   now apply (Rtimes_square_nonneg sor).
   (* PsatzMulC *)
   simpl.
@@ -454,11 +454,11 @@ Proof.
   simpl.
   intro. case_eq (cO [<] c).
   intros.  inversion H1. simpl.
-  rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+  rewrite <- (morph0 (SORrm addon)). now apply cltb_sound.
   discriminate.
   (* PsatzZ *)
   simpl. intros. inversion H0.
-  simpl.   apply  addon.(SORrm).(morph0).
+  simpl.   apply  (morph0 (SORrm addon)).
 Qed.
 
 Fixpoint ge_bool (n m  : nat) : bool :=
@@ -529,8 +529,8 @@ Proof.
   inv H.
   simpl.
   unfold eval_pol.
-  rewrite (Psquare_ok sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))  addon.(SORrm));
+  rewrite (Psquare_ok (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))  (SORrm addon));
   now apply (Rtimes_square_nonneg sor).
   (* PsatzMulC *)
   simpl in *.
@@ -570,12 +570,12 @@ Proof.
   case_eq (cO [<] c).
   intros.  rewrite H1 in H. inv H.
   unfold eval_nformula. simpl.
-  rewrite <- addon.(SORrm).(morph0). now apply cltb_sound.
+  rewrite <- (morph0 (SORrm addon)). now apply cltb_sound.
   intros. rewrite H1 in H. discriminate.
   (* PsatzZ *)
   simpl in *. inv H. 
   unfold eval_nformula. simpl.
-  apply  addon.(SORrm).(morph0).
+  apply  (morph0 (SORrm addon)).
 Qed.
   
 
@@ -592,19 +592,19 @@ Definition psubC := PsubC cminus.
 
 Definition PsubC_ok : forall c P env, eval_pol env (psubC  P c) == eval_pol env P - [c] :=
   let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
-                       sor.(SORplus_wd)
-                       sor.(SORtimes_wd)
-                       sor.(SORopp_wd) in
-                       PsubC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
-                addon.(SORrm).
+                       (SORplus_wd sor)
+                       (SORtimes_wd sor)
+                       (SORopp_wd sor) in
+                       PsubC_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))
+                (SORrm addon).
 
 Definition PaddC_ok : forall c P env, eval_pol env (paddC  P c) == eval_pol env P + [c] :=
   let Rops_wd := mk_reqe (*rplus rtimes ropp req*)
-                       sor.(SORplus_wd)
-                       sor.(SORtimes_wd)
-                       sor.(SORopp_wd) in
-                       PaddC_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt))
-                addon.(SORrm).
+                       (SORplus_wd sor)
+                       (SORtimes_wd sor)
+                       (SORopp_wd sor) in
+                       PaddC_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor))
+                (SORrm addon).
 
 
 (* Check that a formula f is inconsistent by normalizing and comparing the
@@ -631,9 +631,9 @@ intros p op H1 env. unfold check_inconsistent in H1.
 destruct op; simpl ;
 (*****)
 destruct p ; simpl; try discriminate H1;
-try rewrite <- addon.(SORrm).(morph0); trivial.
+try rewrite <- (morph0 (SORrm addon)); trivial.
 now apply cneqb_sound.
-apply addon.(SORrm).(morph_eq) in H1. congruence.
+apply (morph_eq (SORrm addon)) in H1. congruence.
 apply cleb_sound in H1. now apply -> (Rle_ngt sor).
 apply cltb_sound in H1. now apply -> (Rlt_nge sor).
 Qed.
@@ -736,21 +736,21 @@ let (lhs, op, rhs) := f in
 Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) == eval_pol env lhs - eval_pol env rhs.
 Proof.
   intros.
-  apply (Psub_ok  sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+  apply (Psub_ok  (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)).
 Qed.
 
 Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd  lhs rhs) == eval_pol env lhs + eval_pol env rhs.
 Proof.
   intros.
-  apply (Padd_ok  sor.(SORsetoid) Rops_wd
-    (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)).
+  apply (Padd_ok  (SORsetoid sor) Rops_wd
+    (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)).
 Qed.
 
 Lemma eval_pol_norm : forall env lhs, eval_pexpr env lhs == eval_pol env  (norm lhs).
 Proof.
   intros.
-  apply  (norm_aux_spec sor.(SORsetoid) Rops_wd   (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm) addon.(SORpower) ).
+  apply  (norm_aux_spec (SORsetoid sor) Rops_wd   (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon) (SORpower addon) ).
 Qed.
 
 
@@ -805,7 +805,7 @@ Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
   List.map  (fun x => x::nil) (xnormalise t).
 
 
-Add Ring SORRing : sor.(SORrt).
+Add Ring SORRing : (SORrt sor).
 
 Lemma cnf_normalise_correct : forall env t, eval_cnf eval_nformula env (cnf_normalise t) -> eval_formula env t.
 Proof.
@@ -816,7 +816,7 @@ Proof.
     generalize (eval_pexpr  env lhs);
       generalize (eval_pexpr  env rhs) ; intros z1 z2 ; intros.
   (**)
-  apply sor.(SORle_antisymm).
+  apply (SORle_antisymm sor).
   rewrite  (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
   rewrite  (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
   now rewrite <- (Rminus_eq_0 sor).
@@ -855,7 +855,7 @@ Proof.
   rewrite H1 ; ring.
   (**)
   apply H1.
-  apply sor.(SORle_antisymm).
+  apply (SORle_antisymm sor).
   rewrite  (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
   rewrite  (Rle_ngt sor). rewrite (Rlt_lt_minus sor). tauto.
   (**)
@@ -912,7 +912,7 @@ Proof.
   unfold Env.nth.
   unfold jump at 2.
   rewrite <- Pos.add_1_l.
-  rewrite addon.(SORpower).(rpow_pow_N).
+  rewrite (rpow_pow_N (SORpower addon)).
   unfold pow_N. ring.
 Qed.
 
@@ -932,7 +932,7 @@ Proof.
   unfold Env.tail.
   rewrite xdenorm_correct.
   change (Pos.succ xH) with 2%positive.
-  rewrite addon.(SORpower).(rpow_pow_N).
+  rewrite (rpow_pow_N (SORpower addon)).
   simpl. reflexivity.
 Qed.
 
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 137453a9ed..9ff6850fdf 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -43,48 +43,48 @@ Notation "x < y" := (rlt x y).
 
 Lemma req_refl : forall x, req x x.
 Proof.
-  destruct sor.(SORsetoid) as (Equivalence_Reflexive,_,_).
+  destruct (SORsetoid sor) as (Equivalence_Reflexive,_,_).
   apply Equivalence_Reflexive.
 Qed.
 
 Lemma req_sym : forall x y, req x y -> req y x.
 Proof.
-  destruct sor.(SORsetoid) as (_,Equivalence_Symmetric,_).
+  destruct (SORsetoid sor) as (_,Equivalence_Symmetric,_).
   apply Equivalence_Symmetric.
 Qed.
 
 Lemma req_trans : forall x y z, req x y -> req y z -> req x z.
 Proof.
-  destruct sor.(SORsetoid) as (_,_,Equivalence_Transitive).
+  destruct (SORsetoid sor) as (_,_,Equivalence_Transitive).
   apply Equivalence_Transitive.
 Qed.
 
 
 Add Relation R req
-  reflexivity proved by sor.(SORsetoid).(@Equivalence_Reflexive _ _)
-  symmetry proved by sor.(SORsetoid).(@Equivalence_Symmetric _ _)
-  transitivity proved by sor.(SORsetoid).(@Equivalence_Transitive _ _)
+  reflexivity proved by (@Equivalence_Reflexive _ _ (SORsetoid sor))
+  symmetry proved by (@Equivalence_Symmetric _ _ (SORsetoid sor))
+  transitivity proved by (@Equivalence_Transitive _ _ (SORsetoid sor))
 as sor_setoid.
 
 Add Morphism rplus with signature req ==> req ==> req as rplus_morph.
 Proof.
-exact sor.(SORplus_wd).
+exact (SORplus_wd sor).
 Qed.
 Add Morphism rtimes with signature req ==> req ==> req as rtimes_morph.
 Proof.
-exact sor.(SORtimes_wd).
+exact (SORtimes_wd sor).
 Qed.
 Add Morphism ropp with signature req ==> req as ropp_morph.
 Proof.
-exact sor.(SORopp_wd).
+exact (SORopp_wd sor).
 Qed.
 Add Morphism rle with signature req ==> req ==> iff as rle_morph.
 Proof.
-exact sor.(SORle_wd).
+exact (SORle_wd sor).
 Qed.
 Add Morphism rlt with signature req ==> req ==> iff as rlt_morph.
 Proof.
-exact sor.(SORlt_wd).
+exact (SORlt_wd sor).
 Qed.
 Add Morphism rminus with signature req ==> req ==> req as rminus_morph.
 Proof.
@@ -115,7 +115,7 @@ Lemma Zring_morph :
              0%Z 1%Z Z.add Z.mul Z.sub Z.opp
              Zeq_bool gen_order_phi_Z.
 Proof.
-exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
+exact (gen_phiZ_morph (SORsetoid sor) ring_ops_wd (SORrt sor)).
 Qed.
 
 Lemma phi_pos1_pos : forall x : positive, 0 < phi_pos1 x.
@@ -127,8 +127,8 @@ Qed.
 
 Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.
 Proof.
-exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
-        (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
+exact (ARgen_phiPOS_Psucc (SORsetoid sor) ring_ops_wd
+        (Rth_ARth (SORsetoid sor) ring_ops_wd (SORrt sor))).
 Qed.
 
 Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
@@ -142,7 +142,7 @@ Qed.
 Lemma clt_morph : forall x y : Z, (x < y)%Z -> [x] < [y].
 Proof.
 intros x y H.
-do 2 rewrite (same_genZ sor.(SORsetoid) ring_ops_wd sor.(SORrt));
+do 2 rewrite (same_genZ (SORsetoid sor) ring_ops_wd (SORrt sor));
 destruct x; destruct y; simpl in *; try discriminate.
 apply phi_pos1_pos.
 now apply clt_pos_morph.
@@ -157,7 +157,7 @@ Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].
 Proof.
 unfold Z.leb; intros x y H.
 case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
-le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
+le_equal. apply (morph_eq Zring_morph). unfold Zeq_bool; now rewrite H1.
 le_less. now apply clt_morph.
 discriminate.
 Qed.
@@ -172,5 +172,3 @@ apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
 Qed.
 
 End InitialMorphism.
-
-
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index f5d13053b1..813c521ab0 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -54,10 +54,10 @@ Record almost_field_theory : Prop := mk_afield {
 Section AlmostField.
 
 Variable AFth : almost_field_theory.
-Let ARth := AFth.(AF_AR).
-Let rI_neq_rO := AFth.(AF_1_neq_0).
-Let rdiv_def := AFth.(AFdiv_def).
-Let rinv_l := AFth.(AFinv_l).
+Let ARth := (AF_AR AFth).
+Let rI_neq_rO := (AF_1_neq_0 AFth).
+Let rdiv_def := (AFdiv_def AFth).
+Let rinv_l := (AFinv_l AFth).
 
 Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
 Proof. exact (Radd_ext Reqe). Qed.
@@ -115,12 +115,12 @@ Notation "- x" := (copp x) : C_scope.
 Infix "=?" := ceqb : C_scope.
 Notation "[ x ]" := (phi x) (at level 0).
 
-Let phi_0 := CRmorph.(morph0).
-Let phi_1 := CRmorph.(morph1).
+Let phi_0 := (morph0 CRmorph).
+Let phi_1 := (morph1 CRmorph).
 
 Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
 Proof.
-generalize (CRmorph.(morph_eq) c c').
+generalize ((morph_eq CRmorph) c c').
 destruct (c =? c')%coef; auto.
 Qed.
 
@@ -137,7 +137,7 @@ Variable get_sign_spec : sign_theory copp ceqb get_sign.
 Variable cdiv:C -> C -> C*C.
 Variable cdiv_th : div_theory req cadd cmul phi cdiv.
 
-Let rpow_pow := pow_th.(rpow_pow_N).
+Let rpow_pow := (rpow_pow_N pow_th).
 
 (* Polynomial expressions : (PExpr C) *)
 
@@ -428,7 +428,7 @@ Qed.
 
 Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
 Proof.
-induction p;simpl;trivial; now rewrite !CRmorph.(morph_mul), !IHp.
+induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp.
 Qed.
 
 Lemma pow_pos_mul_l x y p :
@@ -1587,7 +1587,7 @@ Section FieldAndSemiField.
 
   Definition F2AF f :=
     mk_afield
-      (Rth_ARth Rsth Reqe f.(F_R)) f.(F_1_neq_0) f.(Fdiv_def) f.(Finv_l).
+      (Rth_ARth Rsth Reqe (F_R f)) (F_1_neq_0 f) (Fdiv_def f) (Finv_l f).
 
   Record semi_field_theory : Prop := mk_sfield {
     SF_SR : semi_ring_theory rO rI radd rmul req;
@@ -1603,10 +1603,10 @@ End MakeFieldPol.
   Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth
     (sf:semi_field_theory rO rI radd rmul rdiv rinv req)  :=
     mk_afield _ _
-      (SRth_ARth Rsth sf.(SF_SR))
-      sf.(SF_1_neq_0)
-      sf.(SFdiv_def)
-      sf.(SFinv_l).
+      (SRth_ARth Rsth (SF_SR sf))
+      (SF_1_neq_0 sf)
+      (SFdiv_def sf)
+      (SFinv_l sf).
 
 
 Section Complete.
@@ -1621,9 +1621,9 @@ Section Complete.
   Notation "x == y" := (req x y) (at level 70, no associativity).
  Variable Rsth : Setoid_Theory R req.
    Add Parametric Relation : R req
-     reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
-     symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
-     transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+     reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
+     symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
+     transitivity proved by (@Equivalence_Transitive _ _ Rsth)
     as R_setoid3.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
    Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
@@ -1636,10 +1636,10 @@ Section Complete.
 Section AlmostField.
 
  Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
- Let ARth := AFth.(AF_AR).
- Let rI_neq_rO := AFth.(AF_1_neq_0).
- Let rdiv_def := AFth.(AFdiv_def).
- Let rinv_l := AFth.(AFinv_l).
+ Let ARth := (AF_AR AFth).
+ Let rI_neq_rO := (AF_1_neq_0 AFth).
+ Let rdiv_def := (AFdiv_def AFth).
+ Let rinv_l := (AFinv_l AFth).
 
 Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
 
@@ -1705,10 +1705,10 @@ End AlmostField.
 Section Field.
 
  Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
- Let Rth := Fth.(F_R).
- Let rI_neq_rO := Fth.(F_1_neq_0).
- Let rdiv_def := Fth.(Fdiv_def).
- Let rinv_l := Fth.(Finv_l).
+ Let Rth := (F_R Fth).
+ Let rI_neq_rO := (F_1_neq_0 Fth).
+ Let rdiv_def := (Fdiv_def Fth).
+ Let rinv_l := (Finv_l Fth).
  Let AFth := F2AF Rsth Reqe Fth.
  Let ARth := Rth_ARth Rsth Reqe Rth.
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 15d490a6ab..4886c8b9aa 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -51,9 +51,9 @@ Section ZMORPHISM.
   Notation "x == y" := (req x y).
   Variable Rsth : Setoid_Theory R req.
      Add Parametric Relation : R req
-       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
-       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
-       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
+       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
+       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
       as R_setoid3.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
@@ -267,9 +267,9 @@ Section NMORPHISM.
   Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
  Variable Rsth : Setoid_Theory R req.
      Add Parametric Relation : R req
-       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
-       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
-       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
+       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
+       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
        as R_setoid4.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable SReqe : sring_eq_ext radd rmul req.
@@ -392,9 +392,9 @@ Section NWORDMORPHISM.
   Notation "x == y" := (req x y).
   Variable Rsth : Setoid_Theory R req.
      Add Parametric Relation : R req
-       reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
-       symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
-       transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
+       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
+       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
       as R_setoid5.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
@@ -581,9 +581,9 @@ Section GEN_DIV.
 
   (* Useful tactics *)
   Add Parametric Relation : R req
-    reflexivity  proved by Rsth.(@Equivalence_Reflexive _ _)
-    symmetry     proved by Rsth.(@Equivalence_Symmetric _ _)
-    transitivity proved by Rsth.(@Equivalence_Transitive _ _)
+    reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
+    symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
+    transitivity proved by (@Equivalence_Transitive _ _ Rsth)
    as R_set1.
  Ltac rrefl := gen_reflexivity Rsth.
   Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
@@ -614,7 +614,7 @@ Section GEN_DIV.
  Proof.
   constructor.
   intros a b;unfold triv_div.
-  assert (X:= morph.(morph_eq) a b);destruct (ceqb a b).
+  assert (X:= morph_eq morph a b);destruct (ceqb a b).
   Esimpl.
   rewrite X; trivial.
   rsimpl.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 12f716c496..f7cb6b688b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -600,7 +600,7 @@ Section MakeRingPol.
  Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
  Proof.
   rewrite Pos.add_comm.
-  apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
+  apply (pow_pos_add Rsth (Rmul_ext Reqe) (ARmul_assoc ARth)).
  Qed.
 
  Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
@@ -810,7 +810,7 @@ Section MakeRingPol.
  Proof.
  revert l.
  induction P as [c0 | j P IH | P1 IH1 i P2 IH2]; intros l; Esimpl. 
- - assert (H := div_th.(div_eucl_th) c0 c). 
+ - assert (H := (div_eucl_th div_th) c0 c).
    destruct cdiv as (q,r). rewrite H; Esimpl. add_permut. 
  - destr_factor. Esimpl.
  - destr_factor. Esimpl. add_permut.
@@ -827,7 +827,7 @@ Section MakeRingPol.
   try (case Pos.compare_spec; intros He);
   rewrite ?He;
    destr_factor; simpl; Esimpl.
- - assert (H := div_th.(div_eucl_th) c0 c).
+ - assert (H := div_eucl_th div_th c0 c).
    destruct cdiv as (q,r). rewrite H; Esimpl. add_permut.
  - assert (H := Mcphi_ok P c). destr_factor. Esimpl.
  - now rewrite <- jump_add, Pos.sub_add.
@@ -1073,7 +1073,7 @@ Section POWER.
    - rewrite IHpe1, IHpe2. now rewrite Pmul_ok.
    - rewrite IHpe. Esimpl.
    - rewrite Ppow_N_ok by reflexivity.
-     rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl.
+     rewrite (rpow_pow_N pow_th). destruct n0; simpl; Esimpl.
      induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok.
   Qed.
 
@@ -1329,7 +1329,7 @@ Section POWER.
   case_eq (get_sign c);intros.
   assert (H1 := (morph_eq CRmorph) c0  cI).
   destruct (c0 ?=! cI).
-   rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H)). Esimpl. rewrite H1;trivial.
+   rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H)). Esimpl. rewrite H1;trivial.
    rewrite <- r_list_pow_rev;trivial;Esimpl.
   apply mkmultm1_ok.
  rewrite <- r_list_pow_rev; apply mkmult_rec_ok.
@@ -1340,7 +1340,7 @@ Qed.
  Proof.
   intros;unfold mkadd_mult.
   case_eq (get_sign c);intros.
-  rewrite (CRmorph.(morph_eq) _ _ (get_sign_spec.(sign_spec) _ H));Esimpl.
+  rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H));Esimpl.
   rewrite mkmult_c_pos_ok;Esimpl.
   rewrite mkmult_c_pos_ok;Esimpl.
  Qed.
@@ -1421,7 +1421,7 @@ Qed.
     | xO _ => rpow r (Cp_phi (Npos p))
     | 1 => r
     end == pow_pos rmul r p.
- Proof. destruct p; now rewrite ?pow_th.(rpow_pow_N). Qed.
+ Proof. destruct p; now rewrite ?(rpow_pow_N pow_th). Qed.
 
  Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P  == P@fv.
  Proof.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 6c782269ab..3e835f5c9f 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -358,7 +358,7 @@ Section ALMOST_RING.
   rewrite <-(Radd_0_l Rth (- x * y)).
   rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)).
   rewrite (Radd_assoc Rth), <- (Rdistr_l Rth).
-  rewrite (Rth.(Radd_comm) (-x)), (Ropp_def Rth).
+  rewrite (Radd_comm Rth (-x)), (Ropp_def Rth).
   now rewrite Rmul_0_l, (Radd_0_l Rth).
  Qed.
 
@@ -407,9 +407,9 @@ Section ALMOST_RING.
  Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
 
    Add Parametric Relation : C ceq
-     reflexivity  proved by Csth.(@Equivalence_Reflexive _ _)
-     symmetry     proved by Csth.(@Equivalence_Symmetric _ _)
-     transitivity proved by Csth.(@Equivalence_Transitive _ _)
+     reflexivity  proved by (@Equivalence_Reflexive _ _ Csth)
+     symmetry     proved by (@Equivalence_Symmetric _ _ Csth)
+     transitivity proved by (@Equivalence_Transitive _ _ Csth)
     as C_setoid.
 
    Add Morphism cadd with signature (ceq ==> ceq ==> ceq) as cadd_ext.
@@ -430,7 +430,7 @@ Section ALMOST_RING.
 
  Lemma Smorph_opp x : [-!x] == -[x].
  Proof.
-  rewrite <-  (Rth.(Radd_0_l) [-!x]).
+  rewrite <-  (Radd_0_l Rth [-!x]).
   rewrite <- ((Ropp_def Rth) [x]).
   rewrite ((Radd_comm Rth) [x]).
   rewrite <- (Radd_assoc Rth).
@@ -498,12 +498,12 @@ Qed.
 
  Lemma ARdistr_r x y z : z * (x + y) == z*x + z*y.
  Proof.
-  mrewrite. now rewrite !(ARth.(ARmul_comm) z).
+  mrewrite. now rewrite !(ARmul_comm ARth z).
  Qed.
 
  Lemma ARadd_assoc1 x y z : (x + y) + z == (y + z) + x.
  Proof.
-  now rewrite <-(ARth.(ARadd_assoc) x), (ARth.(ARadd_comm) x).
+  now rewrite <-(ARadd_assoc ARth x), (ARadd_comm ARth x).
  Qed.
 
  Lemma ARadd_assoc2 x y z : (y + x) + z == (y + z) + x.
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6d9e3230a4..fc355c2c79 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -103,6 +103,8 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
+let is_projection cst = Cmap.mem cst !projection_table
+
 let prim_table =
   Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3e43372b65..76d36c9b62 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -44,6 +44,8 @@ val find_projection_nparams : GlobRef.t -> int
 (** raise [Not_found] if not a projection *)
 val find_projection : GlobRef.t -> struc_typ
 
+val is_projection : Constant.t -> bool
+
 (** Sets up the mapping from constants to primitive projections *)
 val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index 35f8701b2f..135537f8ab 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -96,7 +96,7 @@ Admitted.
 Polymorphic Definition is_unique (A : Type) (x : A) := forall x' : A, x' = x.
 
 Polymorphic Definition InitialObject obj {C : SpecializedCategory obj} (o : C) :=
-    forall o', { m : C.(Morphism) o o' | is_unique m }.
+    forall o', { m : Morphism C o o' | is_unique m }.
 
 Polymorphic Definition SmallCat := ComputableCategory _ SUnderlyingCategory.
 
@@ -136,7 +136,7 @@ Section GraphObj.
 
   Definition UnderlyingGraph_ObjectOf x :=
     match x with
-      | GraphIndexSource => { sd : objC * objC & C.(Morphism) (fst sd) (snd sd) }
+      | GraphIndexSource => { sd : objC * objC & Morphism C (fst sd) (snd sd) }
       | GraphIndexTarget => objC
     end.
 
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 2713e6a188..35f36e87d7 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -1,5 +1,6 @@
 
 Set Printing Projections.
+Set Primitive Projections.
 
 Class HostFunction := host_func : Type.
 
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.