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

7 files changed, 14 insertions, 58 deletions

diff --git a/test-suite/bugs/closed/bug_1362.v b/test-suite/bugs/closed/bug_1362.v
index 6cafb9f0cd..18b8d743b3 100644
--- a/test-suite/bugs/closed/bug_1362.v
+++ b/test-suite/bugs/closed/bug_1362.v
@@ -1,26 +1,17 @@
 (** Omega is now aware of the bodies of context variables
     (of type Z or nat). *)
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z.
 
 Goal let x := 3 in x = 3.
 intros.
-omega.
+lia.
 Qed.
 
 Open Scope nat.
 
 Goal let x := 2 in x = 2.
 intros.
-omega.
+lia.
 Qed.
-
-(** NB: this could be disabled for compatibility reasons *)
-
-Unset Omega UseLocalDefs.
-
-Goal let x := 4 in x = 4.
-intros.
-Fail omega.
-Abort.
diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 0228abbb9b..9f6c8177f6 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,6 +1,6 @@
-Require Import Omega.
+Require Import Lia ZArith.
 
 Goal forall x, Z.succ (Z.pred x) = x.
 intros x.
-omega.
+lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 67ecc3087f..2ebbb66758 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -1,5 +1,5 @@
 
-Require Import ZArith Omega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (** bug 4132: omega was using "simpl" either on whole equations, or on
@@ -14,18 +14,18 @@ Lemma foo
   (H : - zxy' <= zxy)
   (H' : zxy' <= x') : - b <= zxy.
 Proof.
-omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+lia. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
 Qed.
 
 Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "index out of bounds" in the past,
           but I never managed to reproduce that in any version,
           even before my fix. *)
 Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
-omega. (* Pierre L: according to a comment of bug report #4132,
+lia. (* Pierre L: according to a comment of bug report #4132,
           this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/bugs/closed/bug_4717.v b/test-suite/bugs/closed/bug_4717.v
index bd9bac37ef..81bc70d076 100644
--- a/test-suite/bugs/closed/bug_4717.v
+++ b/test-suite/bugs/closed/bug_4717.v
@@ -1,6 +1,6 @@
 (* Omega being smarter on recognizing nat and Z *)
 
-Require Import Omega.
+Require Import Lia ZArith.
 
 Definition nat' := nat.
 
@@ -10,13 +10,13 @@ Theorem le_not_eq_lt : forall (n m:nat),
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Goal forall (x n : nat'), x = x + n - n.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
 
 Open Scope Z_scope.
@@ -29,5 +29,5 @@ Theorem Zle_not_eq_lt : forall n m,
     n < m.
 Proof.
   intros.
-  omega.
+  lia.
 Qed.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
index bad9d64f65..f42e32cf25 100644
--- a/test-suite/bugs/closed/bug_9512.v
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+Require Import Coq.ZArith.BinInt Coq.micromega.Lia.
 
 Set Primitive Projections.
 Record params := { width : Z }.
@@ -10,7 +10,6 @@ Set Printing All.
 Lemma foo : width p = 0%Z -> width p = 0%Z.
   intros.
 
-  assert_succeeds (enough True; [omega|]).
   assert_succeeds (enough True; [lia|]).
 
 (*   H : @eq Z (width p) Z0 *)
@@ -26,12 +25,6 @@ Lemma foo : width p = 0%Z -> width p = 0%Z.
 (*   @eq Z (width p) Z0 *)
 
   assert_succeeds (enough True; [lia|]).
-  (* Tactic failure: <tactic closure> fails. *)
-  (* assert_succeeds (enough True; [omega|]). *)
-  (* Tactic failure: <tactic closure> fails. *)
-
-  (* omega. *)
-  (* Error: Omega can't solve this system *)
 
   lia.
   (* Tactic failure:  Cannot find witness. *)
diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v
deleted file mode 100644
index c045335410..0000000000
--- a/test-suite/bugs/opened/bug_1615.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Require Import Omega.
-
-Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z.
-Proof.
-  intros. omega.
-Qed.
-
-Lemma foo' : forall n m : nat, n <=  n + n * m.
-Proof.
-  intros. Fail omega.
-Abort.
diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v
deleted file mode 100644
index 3690adf90a..0000000000
--- a/test-suite/bugs/opened/bug_6602.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import Omega.
-
-Lemma test_nat:
-  forall n, (5 + pred n <= 5 + n).
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.
-
-Lemma test_N:
-  forall n, (5 + N.pred n <= 5 + n)%N.
-Proof.
-  intros.
-  zify.
-  omega.
-Qed.