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

(warn if bar is a nonprimitive projection)

4 files changed, 52 insertions, 52 deletions

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.