diff options
Diffstat (limited to 'plugins/setoid_ring/Ncring_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 1ca6227f25..aa0370b2ac 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z). Proof. exact Z.eq_equiv. Qed. Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z). +Defined. Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). Proof. |