Deprecate “omega”

9 files changed, 43 insertions, 29 deletions

diff --git a/doc/changelog/04-tactics/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst
new file mode 100644
index 0000000000..59c9612d17
--- /dev/null
+++ b/doc/changelog/04-tactics/11976-deprecate-omega.rst
@@ -0,0 +1,5 @@
+- **Deprecated:**
+  The :tacn:`omega` tactic is deprecated;
+  use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead
+  (`#11976 <https://github.com/coq/coq/pull/11976>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f706633da9..77bf58aac6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -1,4 +1,4 @@
-.. _ micromega:
+.. _micromega:
 
 Micromega: tactics for solving arithmetic goals over ordered rings
 ==================================================================
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index daca43e65e..082ea4691b 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -7,20 +7,18 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
 .. warning::
 
-   The :tacn:`omega` tactic is about to be deprecated in favor of the
-   :tacn:`lia` tactic.  The goal is to consolidate the arithmetic
-   solving capabilities of Coq into a single engine; moreover,
-   :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a
-   complete Presburger arithmetic solver while :tacn:`omega` was known
-   to be incomplete).
-
-   Work is in progress to make sure that there are no regressions
-   (including no performance regression) when switching from
-   :tacn:`omega` to :tacn:`lia` in existing projects.  However, we
-   already recommend using :tacn:`lia` in new or refactored proof
-   scripts.  We also ask that you report (in our `bug tracker
-   <https://github.com/coq/coq/issues>`_) any issue you encounter,
-   especially if the issue was not present in :tacn:`omega`.
+   The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
+   tactic.  The goal is to consolidate the arithmetic solving
+   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
+   in general more powerful than :tacn:`omega` (it is a complete
+   Presburger arithmetic solver while :tacn:`omega` was known to be
+   incomplete).
+
+   It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing
+   projects.  We also ask that you report (in our `bug tracker
+   <https://github.com/coq/coq/issues>`_) any issue you encounter, especially
+   if the issue was not present in :tacn:`omega`.  If no new issues are
+   reported, :tacn:`omega` will be removed soon.
 
    Note that replacing :tacn:`omega` with :tacn:`lia` can break
    non-robust proof scripts which rely on incompleteness bugs of
@@ -31,6 +29,10 @@ Description of ``omega``
 
 .. tacn:: omega
 
+   .. deprecated:: 8.12
+
+      Use :tacn:`lia` instead.
+
    :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
    i.e. for proving formulas made of equations and inequalities over the
    type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers.
@@ -118,7 +120,7 @@ loaded by
 
 .. example::
 
-  .. coqtop:: all
+  .. coqtop:: all warn
 
      Require Import Omega.
 
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 0ace9ef5b9..b63ae32311 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -353,7 +353,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in reset
 
-      Require Import Omega.
+      Require Import Lia.
 
    .. coqtop:: in
 
@@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite g0 g1 g2 using omega : base1.
+      Hint Rewrite g0 g1 g2 using lia : base1.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 62708b01ed..1772362351 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1715,6 +1715,7 @@ performance issue.
 
 .. coqtop:: reset in
 
+   Set Warnings "-omega-is-deprecated".
    Require Import Coq.omega.Omega.
 
    Ltac mytauto := tauto.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 90a991794f..b5d1e8bffd 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2607,7 +2607,7 @@ After the :token:`i_pattern`, a list of binders is allowed.
   .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
-     From Coq Require Import Omega.
+     From Coq Require Import ZArith Lia.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2615,7 +2615,7 @@ After the :token:`i_pattern`, a list of binders is allowed.
   .. coqtop:: all
 
      Lemma test : True.
-     have H x (y : nat) : 2 * x + y = x + x + y by omega.
+     have H x (y : nat) : 2 * x + y = x + x + y by lia.
 
 A proof term provided after ``:=`` can mention these bound variables
 (that are automatically introduced with the given names).
@@ -2625,7 +2625,7 @@ with parentheses even if no type is specified:
 
 .. coqtop:: all restart
 
-   have (x) : 2 * x = x + x by omega.
+   have (x) : 2 * x = x + x by lia.
 
 The :token:`i_item` and :token:`s_item` can be used to interpret the asserted
 hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting
@@ -2668,9 +2668,9 @@ context entry name.
      Arguments Sub {_} _ _.
 
      Lemma test n m (H : m + 1 < n) : True.
-     have @i : 'I_n by apply: (Sub m); omega.
+     have @i : 'I_n by apply: (Sub m); lia.
 
-Note that the subterm produced by :tacn:`omega` is in general huge and
+Note that the subterm produced by :tacn:`lia` is in general huge and
 uninteresting, and hence one may want to hide it.
 For this purpose the ``[: name ]`` intro pattern and the tactic
 ``abstract`` (see :ref:`abstract_ssr`) are provided.
@@ -2680,7 +2680,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic
   .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
-     have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega.
+     have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia.
 
   The type of ``pm`` can be cleaned up by its annotation ``(*1*)`` by just
   simplifying it. The annotations are there for technical reasons only.
@@ -2694,7 +2694,7 @@ with have and an explicit term, they must be used as follows:
 
      Lemma test n m (H : m + 1 < n) : True.
      have [:pm] @i : 'I_n := Sub m pm.
-       by omega.
+       by lia.
 
 In this case the abstract constant ``pm`` is assigned by using it in
 the term that follows ``:=`` and its corresponding goal is left to be
@@ -2712,7 +2712,7 @@ makes use of it).
   .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
-     have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega.
+     have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia.
 
 Last, notice that the use of intro patterns for abstract constants is
 orthogonal to the transparent flag ``@`` for have.
@@ -2963,7 +2963,7 @@ illustrated in the following example.
 
   .. coqtop:: reset none
 
-     From Coq Require Import ssreflect Omega.
+     From Coq Require Import ssreflect Lia.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 2eef459217..79d6c05e1d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1899,8 +1899,15 @@ let destructure_goal =
 
 let destructure_goal = destructure_goal
 
+let warn_omega_is_deprecated =
+  let name = "omega-is-deprecated" in
+  let category = "deprecated" in
+  CWarnings.create ~name ~category (fun () ->
+    Pp.str "omega is deprecated since 8.12; use “lia” instead.")
+
 let omega_solver =
   Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *)
+  warn_omega_is_deprecated ();
   Coqlib.check_required_library ["Coq";"omega";"Omega"];
   reset_all ();
   destructure_goal
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
index 478bc434ad..d9eea2f89d 100644
--- a/theories/Logic/WKL.v
+++ b/theories/Logic/WKL.v
@@ -25,7 +25,7 @@
 Require Import WeakFan List.
 Import ListNotations.
 
-Require Import Omega.
+Require Import Arith.
 
 (** [is_path_from P n l] means that there exists a path of length [n]
     from [l] on which [P] does not hold *)
diff --git a/theories/setoid_ring/Rings_Z.v b/theories/setoid_ring/Rings_Z.v
index f489b00145..372bba7926 100644
--- a/theories/setoid_ring/Rings_Z.v
+++ b/theories/setoid_ring/Rings_Z.v
@@ -11,7 +11,6 @@
 Require Export Cring.
 Require Export Integral_domain.
 Require Export Ncring_initial.
-Require Export Omega.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.