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

(warn if bar is a nonprimitive projection)

8 files changed, 140 insertions, 142 deletions

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.