diff options
| author | Vincent Laporte | 2019-10-28 12:53:39 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:38 +0000 |
| commit | e0e52b72b532b5e487067750b8d860fc2df10df6 (patch) | |
| tree | 82e0d7b327e30ba835acdd7a8f2390ac02d007fe /plugins | |
| parent | c997e97897712e4e55cb4b0238f176bd57ff9374 (diff) | |
setoid_ring: do not use “omega”
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. |