From e0e52b72b532b5e487067750b8d860fc2df10df6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 28 Oct 2019 12:53:39 +0000
Subject: setoid_ring: do not use “omega”

---
 plugins/setoid_ring/Rings_Z.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/setoid_ring')

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. 
-- 
cgit v1.2.3