Remove the omega tactic and related options

1 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 02adb012d9..ef8617cd9e 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -85,19 +85,19 @@ Time Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
         error
   end.
 
-Require Import Omega Setoid.
+Require Import Lia Setoid.
 
 Next Obligation.
   intros ; simpl in *. apply H.
-  simpl in * ; omega.
+  simpl in * ; lia.
 Qed.
 
 Next Obligation. simpl in *; intros.
   revert H0 ; clear_subset_proofs. intros.
-  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst.
+  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by lia. subst.
   revert H0 ; clear_subset_proofs ; tauto.
 
-  apply H. simpl. omega.
+  apply H. simpl. lia.
 Qed.
 
 Program Fixpoint check_n'  (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})