diff options
Diffstat (limited to 'contrib/setoid_ring/InitialRing.v')
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 6542d280c..56b08a8fa 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -243,7 +243,7 @@ Section ZMORPHISM. Zplus Zmult Zeq_bool gen_phiZ). apply mkRmorph;simpl;try rrefl. apply gen_phiZ_add. apply gen_phiZ_mul. apply gen_Zeqb_ok. - apply (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext). + apply (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext). Qed. End ZMORPHISM. |