From a357060331b8806fc2a493e2abc426109f9522a6 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 10 Oct 2019 13:37:12 +0000 Subject: OrderedTypeEx: do not use “omega” --- theories/Structures/OrderedTypeEx.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'theories/Structures') diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index a8e6993a63..cc216b21f8 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -12,7 +12,6 @@ Require Import OrderedType. Require Import ZArith. Require Import PeanoNat. Require Import Ascii String. -Require Import Omega. Require Import NArith Ndec. Require Import Compare_dec. @@ -55,7 +54,7 @@ Module Nat_as_OT <: UsualOrderedType. Proof. unfold lt; intros; apply lt_trans with y; auto. Qed. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - Proof. unfold lt, eq; intros; omega. Qed. + Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. @@ -85,10 +84,10 @@ Module Z_as_OT <: UsualOrderedType. Definition lt (x y:Z) := (x y x ~ x=y. - Proof. intros; omega. Qed. + Proof. intros x y LT ->; revert LT; apply Z.lt_irrefl. Qed. Definition compare x y : Compare lt eq x y. Proof. -- cgit v1.2.3