diff options
| author | Vincent Laporte | 2019-11-05 16:29:24 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:39 +0000 |
| commit | ed89ceb71efa910764290e4017c0ca9cb829eb7c (patch) | |
| tree | 06f0e956311db52a8b4bc4faeef9182c5c16f8bd /test-suite/bugs/opened | |
| parent | b3fc3cbd36570b77af9f17237f30713be861c3ed (diff) | |
Test-suite: avoid using “omega”
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/bug_1596.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v index 27cb731151..89410047b2 100644 --- a/test-suite/bugs/opened/bug_1596.v +++ b/test-suite/bugs/opened/bug_1596.v @@ -1,7 +1,7 @@ Require Import Relations. Require Import FSets. Require Import Arith. -Require Import Omega. +Require Import Lia. Set Keyed Unification. @@ -147,14 +147,14 @@ Module MessageSpi. Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). unfold lt. induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros. - omega. + lia. Qed. Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). unfold eq;unfold lt. induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate H0);injection H0;intros. - elim (lt_irrefl n);try omega. + elim (lt_irrefl n); lia. Qed. Definition compare : forall (x y:t),(Compare lt eq x y). |