diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/Rings_Z.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v index a0901202f7..8a51bcea02 100644 --- a/plugins/setoid_ring/Rings_Z.v +++ b/plugins/setoid_ring/Rings_Z.v @@ -17,8 +17,7 @@ Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. Lemma Z_one_zero: 1%Z <> 0%Z. -omega. -Qed. +Proof. discriminate. Qed. Instance Zdi : (Integral_domain (Rcr:=Zcri)). constructor. |