petites corrections + contournement bug projections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7585 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 119 insertions, 119 deletions

diff --git a/contrib/setoid_ring/Pol.v b/contrib/setoid_ring/Pol.v
index 12d0ffaa2..2bf2574fe 100644
--- a/contrib/setoid_ring/Pol.v
+++ b/contrib/setoid_ring/Pol.v
@@ -40,9 +40,9 @@ Section MakeRingPol.
  (* Usefull tactics *)		  
   Add Setoid R req Rsth as R_set1.
  Ltac rrefl := gen_reflexivity Rsth.
-  Add Morphism radd : radd_ext.  exact Reqe.(Radd_ext). Qed.
-  Add Morphism rmul : rmul_ext.  exact Reqe.(Rmul_ext). Qed.
-  Add Morphism ropp : ropp_ext.  exact Reqe.(Ropp_ext). Qed.
+  Add Morphism radd : radd_ext.  exact (Radd_ext Reqe). Qed.
+  Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
+  Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
   Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
  Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
  Ltac add_push := gen_add_push radd Rsth Reqe ARth.
@@ -388,7 +388,7 @@ Section MakeRingPol.
     (P ?== P') = true -> forall l, P@l == P'@ l.
  Proof.
   induction P;destruct P';simpl;intros;try discriminate;trivial.
-  apply CRmorph.(morph_eq);trivial.
+  apply (morph_eq CRmorph);trivial.
   assert (H1 := Pcompare_Eq_eq p p0); destruct ((p ?= p0)%positive Eq);
    try discriminate H.
   rewrite (IHP P' H); rewrite H1;trivial;rrefl.
@@ -403,12 +403,12 @@ Section MakeRingPol.
 
  Lemma Pphi0 : forall l, P0@l == 0.
  Proof.
-  intros;simpl;apply CRmorph.(morph0).
+  intros;simpl;apply (morph0 CRmorph).
  Qed.
 
  Lemma Pphi1 : forall l,  P1@l == 1.
  Proof.
-  intros;simpl;apply CRmorph.(morph1).
+  intros;simpl;apply (morph1 CRmorph).
  Qed.
 
  Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
@@ -422,8 +422,8 @@ Section MakeRingPol.
  Proof.
   intros l P i Q;unfold mkPX.
   destruct P;try (simpl;rrefl).
-  assert (H := @CRmorph.(morph_eq) c cO);destruct (c ?=! cO);simpl;try rrefl.
-  rewrite (H (refl_equal true));rewrite CRmorph.(morph0).
+  assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl.
+  rewrite (H (refl_equal true));rewrite (morph0 CRmorph).
   rewrite mkPinj_ok;rsimpl;simpl;rrefl.
   assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl.
   rewrite (H (refl_equal true));trivial.
@@ -437,12 +437,12 @@ Section MakeRingPol.
    | |- context [P1@?l] => rewrite (Pphi1 l)
    | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P)
    | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q)
-   | |- context [[cO]] => rewrite CRmorph.(morph0)
-   | |- context [[cI]] => rewrite CRmorph.(morph1)
-   | |- context [[?x +! ?y]] => rewrite (CRmorph.(morph_add) x y)
-   | |- context [[?x *! ?y]] => rewrite (CRmorph.(morph_mul) x y)
-   | |- context [[?x -! ?y]] => rewrite (CRmorph.(morph_sub) x y)
-   | |- context [[-! ?x]] => rewrite (CRmorph.(morph_opp) x)
+   | |- context [[cO]] => rewrite (morph0 CRmorph)
+   | |- context [[cI]] => rewrite (morph1 CRmorph)
+   | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y)
+   | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y)
+   | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y)
+   | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x)
    end));
   rsimpl; simpl. 
  
@@ -470,9 +470,9 @@ Section MakeRingPol.
  Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
  Proof.
   intros c P l; unfold PmulC.
-  assert (H:= @CRmorph.(morph_eq) c cO);destruct (c ?=! cO).
+  assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO).
   rewrite (H (refl_equal true));Esimpl.
-  assert (H1:= @CRmorph.(morph_eq) c cI);destruct (c ?=! cI).
+  assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
   rewrite (H1 (refl_equal true));Esimpl.
   apply PmulC_aux_ok.
  Qed.
@@ -500,7 +500,7 @@ Section MakeRingPol.
   induction P';simpl;intros;Esimpl2.
   generalize P p l;clear P p l.
   induction P;simpl;intros.
-  Esimpl2;apply ARth.(ARadd_sym).
+  Esimpl2;apply (ARadd_sym ARth).
   assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
   rewrite H;Esimpl. rewrite IHP';rrefl.
   rewrite H;Esimpl. rewrite IHP';Esimpl.
@@ -529,9 +529,9 @@ Section MakeRingPol.
   add_push (P3 @ (tl l));rrefl.
   assert (forall P k l, 
            (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k).
-   induction P;simpl;intros;try apply ARth.(ARadd_sym).
-   destruct p2;simpl;try apply ARth.(ARadd_sym).
-   rewrite jump_Pdouble_minus_one;apply ARth.(ARadd_sym).
+   induction P;simpl;intros;try apply (ARadd_sym ARth).
+   destruct p2;simpl;try apply (ARadd_sym ARth).
+   rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth).
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
     rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tl l0));rrefl.
     rewrite IHP'1;simpl;Esimpl.
@@ -553,7 +553,7 @@ Section MakeRingPol.
   induction P';simpl;intros;Esimpl2;trivial.
   generalize P p l;clear P p l.
   induction P;simpl;intros.
-  Esimpl2;apply ARth.(ARadd_sym).
+  Esimpl2;apply (ARadd_sym ARth).
   assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
   rewrite H;Esimpl. rewrite IHP';rsimpl. 
   rewrite H;Esimpl. rewrite IHP';Esimpl.
@@ -583,11 +583,11 @@ Section MakeRingPol.
   assert (forall P k l, 
            (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k).
    induction P;simpl;intros.
-   rewrite Popp_ok;rsimpl;apply ARth.(ARadd_sym);trivial.
+   rewrite Popp_ok;rsimpl;apply (ARadd_sym ARth);trivial.
    destruct p2;simpl;rewrite Popp_ok;rsimpl.
-   apply ARth.(ARadd_sym);trivial.
-   rewrite jump_Pdouble_minus_one;apply ARth.(ARadd_sym);trivial.
-   apply ARth.(ARadd_sym);trivial.
+   apply (ARadd_sym ARth);trivial.
+   rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth);trivial.
+   apply (ARadd_sym ARth);trivial.
     assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
     rewrite IHP'1;rsimpl;add_push (P5 @ (tl l0));rewrite H1;rrefl.
     rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
@@ -609,7 +609,7 @@ Section MakeRingPol.
     (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l).
  Proof.
   induction P;simpl;intros.
-  Esimpl2;apply ARth.(ARmul_sym).
+  Esimpl2;apply (ARmul_sym ARth).
   assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
   rewrite H1; rewrite H;rrefl.
   rewrite H1; rewrite H.
@@ -639,9 +639,9 @@ Section MakeRingPol.
  Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
  Proof.
   destruct P;simpl;intros.
-  Esimpl2;apply ARth.(ARmul_sym).
+  Esimpl2;apply (ARmul_sym ARth).
   rewrite (PmulI_ok P (Pmul_aux_ok P)).
-  apply ARth.(ARmul_sym).
+  apply (ARmul_sym ARth).
   rewrite Padd_ok; Esimpl2.
   rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial.
   rewrite Pmul_aux_ok;mul_push (P' @ l).
@@ -714,7 +714,7 @@ Section MakeRingPol.
   | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l)
   | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l)
   | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe)
-  end;Esimpl2;try rrefl;try apply ARth.(ARadd_sym).
+  end;Esimpl2;try rrefl;try apply (ARadd_sym ARth).
 
  Lemma norm_ok : forall l pe,  PEeval l pe == (norm pe)@l.
  Proof.
@@ -832,16 +832,16 @@ Section MakeRingPol.
   setoid_replace (pow x p * (pow x p * r) ) 
     with (pow x p * pow x p * r);Esimpl.
   unfold rev;simpl. repeat rewrite mkmult_rev_append;simpl.
-  rewrite ARth.(ARmul_sym);rrefl.
+  rewrite (ARmul_sym ARth);rrefl.
  Qed.
 
  Lemma Pphi_add_mult_dev : forall P rP fv lm, 
     rP + P@fv * mkmult1 (rev lm) == add_mult_dev rP P fv lm.
  Proof.
   induction P;simpl;intros.
-  assert (H := CRmorph.(morph_eq) c cI).
+  assert (H := (morph_eq CRmorph) c cI).
    destruct (c ?=! cI).
-    rewrite (H (refl_equal true));rewrite CRmorph.(morph1);Esimpl.
+    rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl.
     destruct (rev lm);Esimpl;rrefl.
     rewrite mkmult1_mkmult;rrefl.
    apply IHP.
@@ -868,9 +868,9 @@ Section MakeRingPol.
 	 P@fv * mkmult1 (rev lm) == mult_dev P fv lm.
  Proof.
   induction P;simpl;intros.
-   assert (H := CRmorph.(morph_eq) c cI).
+   assert (H := (morph_eq CRmorph) c cI).
    destruct (c ?=! cI).
-    rewrite (H (refl_equal true));rewrite CRmorph.(morph1);Esimpl.
+    rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl.
     apply  mkmult1_mkmult.
    apply IHP.
    replace (match P3 with
diff --git a/contrib/setoid_ring/Ring_th.v b/contrib/setoid_ring/Ring_th.v
index 36941e6de..9583dd2d9 100644
--- a/contrib/setoid_ring/Ring_th.v
+++ b/contrib/setoid_ring/Ring_th.v
@@ -162,8 +162,8 @@ Section ALMOST_RING.
  
  Section SEMI_RING.
  Variable SReqe : sring_eq_ext radd rmul req.
-   Add Morphism radd : radd_ext1.  exact SReqe.(SRadd_ext). Qed.
-   Add Morphism rmul : rmul_ext1.  exact SReqe.(SRmul_ext). Qed.
+   Add Morphism radd : radd_ext1.  exact (SRadd_ext SReqe). Qed.
+   Add Morphism rmul : rmul_ext1.  exact (SRmul_ext SReqe). Qed.
  Variable SRth : semi_ring_theory 0 1 radd rmul req.
 
  (** Every semi ring can be seen as an almost ring, by taking :
@@ -177,7 +177,7 @@ Section ALMOST_RING.
 
  Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req.
  Proof.
-  constructor.  exact SReqe.(SRadd_ext). exact SReqe.(SRmul_ext).
+  constructor.  exact (SRadd_ext SReqe). exact (SRmul_ext SReqe).
   exact SRopp_ext.
  Qed.
 
@@ -230,9 +230,9 @@ Section ALMOST_RING.
  End  SEMI_RING.
  
  Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd : radd_ext2.  exact Reqe.(Radd_ext). Qed.
-   Add Morphism rmul : rmul_ext2.  exact Reqe.(Rmul_ext). Qed.
-   Add Morphism ropp : ropp_ext2.  exact Reqe.(Ropp_ext). Qed.
+   Add Morphism radd : radd_ext2.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext2.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext2.  exact (Ropp_ext Reqe). Qed.
  
  Section RING.
  Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
@@ -241,50 +241,50 @@ Section ALMOST_RING.
  Lemma Rmul_0_l : forall x, 0 * x == 0.
  Proof.
   intro x; setoid_replace (0*x) with ((0+1)*x + -x).
-  rewrite Rth.(Radd_0_l); rewrite Rth.(Rmul_1_l).
-  rewrite Rth.(Ropp_def);sreflexivity.
+  rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth).
+  rewrite (Ropp_def Rth);sreflexivity.
 
-  rewrite Rth.(Rdistr_l);rewrite Rth.(Rmul_1_l).
-  rewrite <- Rth.(Radd_assoc); rewrite Rth.(Ropp_def).
-  rewrite Rth.(Radd_sym); rewrite Rth.(Radd_0_l);sreflexivity.
+  rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth).
+  rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth).
+  rewrite (Radd_sym Rth); rewrite (Radd_0_l Rth);sreflexivity.
  Qed.
 
  Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y.
  Proof.
-  intros x y;rewrite <-(Rth.(Radd_0_l) (- x * y)).
-  rewrite Rth.(Radd_sym).
-  rewrite <-(Rth.(Ropp_def) (x*y)).
-  rewrite Rth.(Radd_assoc).
-  rewrite <- Rth.(Rdistr_l).
-  rewrite (Rth.(Radd_sym) (-x));rewrite Rth.(Ropp_def).
-  rewrite Rmul_0_l;rewrite Rth.(Radd_0_l);sreflexivity.
+  intros x y;rewrite <-(Radd_0_l Rth (- x * y)).
+  rewrite (Radd_sym Rth).
+  rewrite <-(Ropp_def Rth (x*y)).
+  rewrite (Radd_assoc Rth).
+  rewrite <- (Rdistr_l Rth).
+  rewrite (Rth.(Radd_sym) (-x));rewrite (Ropp_def Rth).
+  rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity.
  Qed.
  
  Lemma Ropp_add : forall x y, -(x + y) == -x + -y.
  Proof.
-  intros x y;rewrite <- (Rth.(Radd_0_l) (-(x+y))).
-  rewrite <- (Rth.(Ropp_def) x).
-  rewrite <- (Rth.(Radd_0_l) (x + - x + - (x + y))).
-  rewrite <- (Rth.(Ropp_def) y).
-  rewrite (Rth.(Radd_sym) x).
-  rewrite (Rth.(Radd_sym) y).
-  rewrite <- (Rth.(Radd_assoc) (-y)).
-  rewrite <- (Rth.(Radd_assoc) (- x)).
-  rewrite (Rth.(Radd_assoc)  y).
-  rewrite (Rth.(Radd_sym) y).
-  rewrite <- (Rth.(Radd_assoc)  (- x)).
-  rewrite (Rth.(Radd_assoc) y).
-  rewrite (Rth.(Radd_sym) y);rewrite Rth.(Ropp_def).
-  rewrite (Rth.(Radd_sym) (-x) 0);rewrite Rth.(Radd_0_l).
-  apply Rth.(Radd_sym).
+  intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))).
+  rewrite <- ((Ropp_def Rth) x).
+  rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))).
+  rewrite <- ((Ropp_def Rth) y).
+  rewrite ((Radd_sym Rth) x).
+  rewrite ((Radd_sym Rth) y).
+  rewrite <- ((Radd_assoc Rth) (-y)).
+  rewrite <- ((Radd_assoc Rth) (- x)).
+  rewrite ((Radd_assoc Rth)  y).
+  rewrite ((Radd_sym Rth) y).
+  rewrite <- ((Radd_assoc Rth)  (- x)).
+  rewrite ((Radd_assoc Rth) y).
+  rewrite ((Radd_sym Rth) y);rewrite (Ropp_def Rth).
+  rewrite ((Radd_sym Rth) (-x) 0);rewrite (Radd_0_l Rth).
+  apply (Radd_sym Rth).
  Qed.
  
  Lemma Ropp_opp : forall x, - -x == x.
  Proof.
   intros x; rewrite <- (Radd_0_l Rth (- -x)).
   rewrite <- (Ropp_def Rth x).
-  rewrite <- Rth.(Radd_assoc); rewrite Rth.(Ropp_def).
-  rewrite (Rth.(Radd_sym) x);apply Rth.(Radd_0_l).
+  rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth).
+  rewrite ((Radd_sym Rth) x);apply (Radd_0_l Rth).
  Qed.
 
  Lemma  Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
@@ -304,9 +304,9 @@ Section ALMOST_RING.
  Variable Csth : Setoid_Theory C ceq.
  Variable Ceqe : ring_eq_ext cadd cmul copp ceq.
    Add Setoid C ceq Csth as C_setoid.
-   Add Morphism cadd : cadd_ext.  exact Ceqe.(Radd_ext). Qed.
-   Add Morphism cmul : cmul_ext.  exact Ceqe.(Rmul_ext). Qed.
-   Add Morphism copp : copp_ext.  exact Ceqe.(Ropp_ext). Qed.
+   Add Morphism cadd : cadd_ext.  exact (Radd_ext Ceqe). Qed.
+   Add Morphism cmul : cmul_ext.  exact (Rmul_ext Ceqe). Qed.
+   Add Morphism copp : copp_ext.  exact (Ropp_ext Ceqe). Qed.
  Variable Cth : ring_theory cO cI cadd cmul csub copp ceq.
  Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi.
  Variable phi_ext : forall x y, ceq x y -> [x] == [y].
@@ -314,20 +314,20 @@ Section ALMOST_RING.
  Lemma Smorph_opp : forall x, [-!x] == -[x].
  Proof.
   intros x;rewrite <-  (Rth.(Radd_0_l) [-!x]).
-  rewrite <- (Rth.(Ropp_def) [x]).
-  rewrite (Rth.(Radd_sym) [x]).
-  rewrite <- Rth.(Radd_assoc).
-  rewrite <- Smorph.(Smorph_add).
-  rewrite (Cth.(Ropp_def)).
-  rewrite Smorph.(Smorph0).
+  rewrite <- ((Ropp_def Rth) [x]).
+  rewrite ((Radd_sym Rth) [x]).
+  rewrite <- (Radd_assoc Rth).
+  rewrite <- (Smorph_add Smorph).
+  rewrite (Ropp_def Cth).
+  rewrite (Smorph0 Smorph).
   rewrite (Radd_sym Rth (-[x])).
-  apply Rth.(Radd_0_l);sreflexivity.
+  apply (Radd_0_l Rth);sreflexivity.
  Qed. 
 
  Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y].
  Proof.
-  intros x y; rewrite Cth.(Rsub_def);rewrite Rth.(Rsub_def).
-  rewrite Smorph.(Smorph_add);rewrite Smorph_opp;sreflexivity.
+  intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth).
+  rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity.
  Qed.
 
  Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req 
@@ -350,23 +350,23 @@ Section ALMOST_RING.
   setoid_replace (x1 - y1) with (x1 + -y1). 
   setoid_replace (x2 - y2) with (x2 + -y2).
   rewrite H;rewrite H0;sreflexivity.
-  apply ARth.(ARsub_def).
-  apply ARth.(ARsub_def).
+  apply (ARsub_def ARth).
+  apply (ARsub_def ARth).
  Qed.
    Add Morphism rsub : rsub_ext.  exact ARsub_ext. Qed.
 
  Ltac mrewrite :=
    repeat first
-     [ rewrite ARth.(ARadd_0_l)
-     | rewrite <- (ARth.(ARadd_sym) 0)
-     | rewrite ARth.(ARmul_1_l)
-     | rewrite <- (ARth.(ARmul_sym) 1)
-     | rewrite ARth.(ARmul_0_l)
-     | rewrite <- (ARth.(ARmul_sym) 0)
-     | rewrite ARth.(ARdistr_l)
+     [ rewrite (ARadd_0_l ARth)
+     | rewrite <- ((ARadd_sym ARth) 0)
+     | rewrite (ARmul_1_l ARth)
+     | rewrite <- ((ARmul_sym ARth) 1)
+     | rewrite (ARmul_0_l ARth)
+     | rewrite <- ((ARmul_sym ARth) 0)
+     | rewrite (ARdistr_l ARth)
      | sreflexivity
      | match goal with
-       | |- context [?z * (?x + ?y)] => rewrite (ARth.(ARmul_sym) z (x+y))
+       | |- context [?z * (?x + ?y)] => rewrite ((ARmul_sym ARth) z (x+y))
        end].
  
  Lemma ARadd_0_r : forall x, (x + 0) == x.
@@ -392,31 +392,31 @@ Section ALMOST_RING.
 
  Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
  Proof.
-  intros; repeat rewrite <- ARth.(ARadd_assoc);
-   rewrite (ARth.(ARadd_sym) x); sreflexivity.
+  intros; repeat rewrite <- (ARadd_assoc ARth);
+   rewrite ((ARadd_sym ARth) x); sreflexivity.
  Qed.
 
  Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x.
  Proof.
-  intros;rewrite <-(ARth.(ARmul_assoc) x).
-  rewrite (ARth.(ARmul_sym) x);sreflexivity.
+  intros;rewrite <-((ARmul_assoc ARth) x).
+  rewrite ((ARmul_sym ARth) x);sreflexivity.
  Qed.
  
  Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x.
  Proof.
-  intros; repeat rewrite <- ARth.(ARmul_assoc);
-   rewrite (ARth.(ARmul_sym) x); sreflexivity.
+  intros; repeat rewrite <- (ARmul_assoc ARth);
+   rewrite ((ARmul_sym ARth) x); sreflexivity.
  Qed.
 
  Lemma ARopp_mul_r : forall x y,  - (x * y) == x * -y.
  Proof.
-  intros;rewrite (ARth.(ARmul_sym) x y);
-   rewrite ARth.(ARopp_mul_l); apply ARth.(ARmul_sym).
+  intros;rewrite ((ARmul_sym ARth) x y);
+   rewrite (ARopp_mul_l ARth); apply (ARmul_sym ARth).
  Qed.
 
  Lemma ARopp_zero : -0 == 0.
  Proof.
-  rewrite <- (ARmul_0_r 0); rewrite ARth.(ARopp_mul_l).
+  rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth).
   repeat rewrite ARmul_0_r; sreflexivity.
  Qed.
 
@@ -429,19 +429,19 @@ Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth :=
   repeat first
      [ gen_reflexivity Rsth
      | progress rewrite (ARopp_zero Rsth Reqe ARth)
-     | rewrite ARth.(ARadd_0_l)
+     | rewrite (ARadd_0_l ARth)
      | rewrite (ARadd_0_r Rsth ARth)
-     | rewrite ARth.(ARmul_1_l)
+     | rewrite (ARmul_1_l ARth)
      | rewrite (ARmul_1_r Rsth ARth)
-     | rewrite ARth.(ARmul_0_l)
+     | rewrite (ARmul_0_l ARth)
      | rewrite (ARmul_0_r Rsth ARth)
-     | rewrite ARth.(ARdistr_l)
+     | rewrite (ARdistr_l ARth)
      | rewrite (ARdistr_r Rsth Reqe ARth)
-     | rewrite ARth.(ARadd_assoc)
-     | rewrite ARth.(ARmul_assoc)
-     | progress rewrite ARth.(ARopp_add)
-     | progress rewrite ARth.(ARsub_def)
-     | progress rewrite <- ARth.(ARopp_mul_l)
+     | rewrite (ARadd_assoc ARth)
+     | rewrite (ARmul_assoc ARth)
+     | progress rewrite (ARopp_add ARth)
+     | progress rewrite (ARsub_def ARth)
+     | progress rewrite <- (ARopp_mul_l ARth)
      | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ].
 
 Ltac gen_add_push add Rsth Reqe ARth x :=
diff --git a/contrib/setoid_ring/ZRing_th.v b/contrib/setoid_ring/ZRing_th.v
index 48a56c841..9060428b9 100644
--- a/contrib/setoid_ring/ZRing_th.v
+++ b/contrib/setoid_ring/ZRing_th.v
@@ -44,9 +44,9 @@ Section ZMORPHISM.
      Add Setoid R req Rsth as R_setoid3.
      Ltac rrefl := gen_reflexivity Rsth.
  Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd : radd_ext3.  exact Reqe.(Radd_ext). Qed.
-   Add Morphism rmul : rmul_ext3.  exact Reqe.(Rmul_ext). Qed.
-   Add Morphism ropp : ropp_ext3.  exact Reqe.(Ropp_ext). Qed.
+   Add Morphism radd : radd_ext3.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext3.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext3.  exact (Ropp_ext Reqe). Qed.
 
  Fixpoint gen_phiPOS1 (p:positive) : R :=
   match p with
@@ -162,15 +162,15 @@ Section ZMORPHISM.
   replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
   rewrite <- Pcompare_antisym in H1.
   destruct ((x ?= y)%positive Eq).
-  rewrite H;trivial. rewrite Rth.(Ropp_def);rrefl.
+  rewrite H;trivial. rewrite (Ropp_def Rth);rrefl.
   destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
   unfold Pminus; rewrite Heq1;rewrite <- Heq2.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  rewrite Rth.(Ropp_def);norm.
+  rewrite (Ropp_def Rth);norm.
   destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
   unfold Pminus; rewrite Heq1;rewrite <- Heq2.
   rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  add_push (gen_phiPOS1 h);rewrite Rth.(Ropp_def); norm.
+  add_push (gen_phiPOS1 h);rewrite (Ropp_def Rth); norm.
  Qed.
 
  Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
@@ -187,7 +187,7 @@ Section ZMORPHISM.
   replace Eq with (CompOpp Eq);trivial.
   rewrite <- Pcompare_antisym;simpl.
   rewrite match_compOpp.    
-  rewrite Rth.(Radd_sym).
+  rewrite (Radd_sym Rth).
   apply gen_phiZ1_add_pos_neg.
   rewrite (ARgen_phiPOS_add ARth); norm.
  Qed.
@@ -274,9 +274,9 @@ Section NMORPHISM.
  Let rsub := (@SRsub R radd).
   Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
   Notation "x == y" := (req x y).
-   Add Morphism radd : radd_ext4.  exact Reqe.(Radd_ext). Qed.
-   Add Morphism rmul : rmul_ext4.  exact Reqe.(Rmul_ext). Qed.
-   Add Morphism ropp : ropp_ext4.  exact Reqe.(Ropp_ext). Qed.
+   Add Morphism radd : radd_ext4.  exact (Radd_ext Reqe). Qed.
+   Add Morphism rmul : rmul_ext4.  exact (Rmul_ext Reqe). Qed.
+   Add Morphism ropp : ropp_ext4.  exact (Ropp_ext Reqe). Qed.
    Add Morphism rsub : rsub_ext5.  exact (ARsub_ext Rsth Reqe ARth). Qed.
    Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.