Merge PR #13741: Remove omega tactic (deprecated in 8.12)

Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: silene
Ack-by: SkySkimmer
Ack-by: olaure01

1 files changed, 9 insertions, 9 deletions

diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index d2e6794c0b..1f4913b49d 100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
@@ -140,35 +140,35 @@ Qed.
 Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma lt_minus_eq_0 : forall m n : nat, m < n -> m - n = 0.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_Sn_1_SSn : forall n : nat, S n + 1 <= S (S n).
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
 Proof. 
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
 Proof. 
- intros; omega.
+ intros; lia.
 Qed.
 
 Lemma minus_pred : forall m n : nat, 0 < n -> pred m - pred n = m - n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -1414,13 +1414,13 @@ Qed.
 Lemma lt_inj : forall m n : nat, (m < n)%Z -> m < n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 Lemma le_inj : forall m n : nat, (m <= n)%Z -> m <= n.
 Proof.
  intros.
- omega.
+ lia.
 Qed.
 
 
@@ -1501,7 +1501,7 @@ Proof.
   [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1));
      [ idtac | apply f_equal with Z; auto with zarith ];
      rewrite absolu_plus;
-     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega
+     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; lia
      | auto with zarith
      | intro; discriminate ]
   | rewrite <- H1; reflexivity ].