From ed89ceb71efa910764290e4017c0ca9cb829eb7c Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 5 Nov 2019 16:29:24 +0000
Subject: Test-suite: avoid using “omega”

---
 test-suite/bugs/opened/bug_1596.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/bugs/opened')

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).
-- 
cgit v1.2.3