diff options
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). |