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

(warn if bar is a nonprimitive projection)

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