diff options
| author | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
| commit | ac8633ba19a7d8e937bbd6f9b7de2ad82b89f22f (patch) | |
| tree | b6512ba01f5b00fe490fe90b9d848c0d8a4c1f80 /theories/Structures | |
| parent | 487f23187413e6cf6ee117d798a9057d0008aa6a (diff) | |
| parent | 4af9a79457fc265b1696de2b1fa1018ef12c986a (diff) | |
Merge PR #10875: [Stdlib] Remove some uses of the “omega” tactic
Reviewed-by: fajb
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedTypeEx.v | 7 |
1 files changed, 3 insertions, 4 deletions
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). Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. - Proof. intros; omega. Qed. + Proof. exact Z.lt_trans. Qed. Lemma lt_not_eq : forall x y, x<y -> ~ 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. |