Test-suite: avoid using “omega”

8 files changed, 26 insertions, 26 deletions

diff --git a/test-suite/bugs/closed/bug_2083.v b/test-suite/bugs/closed/bug_2083.v
index f33e96cea6..40fda71e66 100644
--- a/test-suite/bugs/closed/bug_2083.v
+++ b/test-suite/bugs/closed/bug_2083.v
@@ -13,15 +13,15 @@ Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
         error
   end.
 
-Require Import Omega.
+Require Import Lia.
 
-Solve Obligations with program_simpl ; auto with *; try omega.
+Solve Obligations with program_simpl ; auto with *; lia.
 
 Next Obligation.
-  apply H. simpl. omega.
+  apply H. simpl. lia.
 Defined.
 
 Next Obligation.
-  case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
+  case (le_lt_dec p i) ; intros. assert(i = p) by lia. subst.
   revert H0. clear_subset_proofs. auto.
   apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/bug_3652.v b/test-suite/bugs/closed/bug_3652.v
index 915cfcac27..b21a4d939c 100644
--- a/test-suite/bugs/closed/bug_3652.v
+++ b/test-suite/bugs/closed/bug_3652.v
@@ -1,6 +1,7 @@
 Require Setoid.
 Require ZArith.
 Import ZArith.
+Require Import Lia.
 
 Inductive Erasable(A : Set) : Prop :=
   erasable: A -> Erasable A.
@@ -87,12 +88,12 @@ Proof.
     unfold zotval.
     unfold mp2a1s.
     ring_simplify'.
-    replace 2 with (2*1) at 2 7 by omega.
+    replace 2 with (2*1) at 2 7 by lia.
     rewrite <-?Z.mul_assoc.
     rewrite <-?Z.mul_add_distr_l.
     rewrite <-Z.mul_sub_distr_l.
-    rewrite Z.mul_cancel_l by omega.
-    replace 1 with (2-1) at 1 by omega.
+    rewrite Z.mul_cancel_l by lia.
+    replace 1 with (2-1) at 1 by lia.
     rewrite Z.add_sub_assoc.
     rewrite Z.sub_cancel_r.
     Unshelve.
diff --git a/test-suite/bugs/closed/bug_4280.v b/test-suite/bugs/closed/bug_4280.v
index fd7897509e..31524e5dcf 100644
--- a/test-suite/bugs/closed/bug_4280.v
+++ b/test-suite/bugs/closed/bug_4280.v
@@ -1,11 +1,11 @@
-Require Import ZArith.
+Require Import ZArith Lia.
 Require Import Eqdep_dec.
 Local Open Scope Z_scope.
 
 Definition t := { n: Z | n > 1 }.
 
 Program Definition two : t := 2.
-Next Obligation. omega. Qed.
+Next Obligation. lia. Qed.
 
 Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
   if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v
index f1bce04451..1ad84f9bb5 100644
--- a/test-suite/bugs/closed/bug_4306.v
+++ b/test-suite/bugs/closed/bug_4306.v
@@ -1,7 +1,7 @@
 Require Import List.
 Require Import Arith.
 Require Import Recdef.
-Require Import Omega.
+Require Import Lia.
 
 Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
   match xys with
@@ -14,9 +14,7 @@ Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
                               end
   end.
 Proof.
-  intros; simpl; omega.
-  intros; simpl; omega.
-  intros; simpl; omega.
+  all: simpl; lia.
 Qed.
 
 Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v
index 7685552725..0c26d4de32 100644
--- a/test-suite/bugs/closed/bug_4456.v
+++ b/test-suite/bugs/closed/bug_4456.v
@@ -10,7 +10,7 @@ Tactic Notation "admit" := case proof_admitted.
 
 Require Coq.Program.Program.
 Require Coq.Strings.String.
-Require Coq.omega.Omega.
+Require Coq.micromega.Lia.
 Module Export Fiat_DOT_Common.
 Module Export Fiat.
 Module Common.
@@ -489,7 +489,8 @@ Defined.
   End app.
 
 Import Coq.Lists.List.
-Import Coq.omega.Omega.
+Import Coq.Arith.Arith.
+Import Coq.micromega.Lia.
 Import Fiat_DOT_Common.Fiat.Common.
 Import Fiat.Parsers.ContextFreeGrammar.Valid.
 Local Open Scope string_like_scope.
@@ -585,8 +586,8 @@ Defined.
               | _ => discriminate
               | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z))
               | _ => solve [ eauto with nocore ]
-              | _ => solve [ apply Min.min_case_strong; omega ]
-              | _ => omega
+              | _ => solve [ apply Min.min_case_strong; lia ]
+              | _ => lia
               | [ H : production_valid (_::_) |- _ ]
                 => let H' := fresh in
                    pose proof H as H';
diff --git a/test-suite/bugs/closed/bug_4852.v b/test-suite/bugs/closed/bug_4852.v
index e2e00f05d3..cdc8cd8b20 100644
--- a/test-suite/bugs/closed/bug_4852.v
+++ b/test-suite/bugs/closed/bug_4852.v
@@ -2,7 +2,7 @@
 
 Require Import Coq.Lists.List.
 Import ListNotations.
-Require Import Omega.
+Require Import Lia.
 
 Definition wfi_lt := well_founded_induction_type Wf_nat.lt_wf.
 
@@ -16,7 +16,7 @@ Tactic Notation "wfinduction" constr(term) "on" ne_hyp_list(Hs) "as" ident(H) :=
 
 Hint Rewrite @app_comm_cons @app_assoc @app_length : app_rws.
 
-Ltac solve_nat := autorewrite with app_rws in *; cbn in *; omega.
+Ltac solve_nat := autorewrite with app_rws in *; cbn in *; lia.
 
 Notation "| x |" := (length x) (at level 11, no associativity, format "'|' x '|'").
 
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).
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 61ae4edbd1..398528de72 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,7 +16,7 @@ Check
     end
   in f 0.
 
-Require Import ZArith_base Omega.
+Require Import ZArith_base Lia.
 Open Scope Z_scope.
 
 Inductive even: Z -> Prop :=
@@ -35,13 +35,13 @@ Proof.
 fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
  intros.
  destruct H.
-   omega.
+   lia.
    apply odd_pos_even_pos in H.
-   omega.
+   lia.
  intros.
  destruct H.
   apply even_pos_odd_pos in H.
-  omega.
+  lia.
 Qed.
 
 CoInductive Inf := S { projS : Inf }.