diff options
| author | Emilio Jesus Gallego Arias | 2019-11-29 17:12:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-29 17:12:16 +0100 |
| commit | 37b1348d54df2d65389987e8bd920f9e1b275c44 (patch) | |
| tree | f651a6c919c078744af13fed4eaff6e20e54389b /plugins/setoid_ring | |
| parent | 18ad1b309bbdcf8aa4cc12b024b88007dfd9c14f (diff) | |
| parent | ed89ceb71efa910764290e4017c0ca9cb829eb7c (diff) | |
Merge PR #11076: Remove all remaining calls to “omega” from the standard library
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/setoid_ring')
| -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. |