[refman] Remove references to omega from Tactics chapter.

Omega was defined twice and this is the tactics chapter documentation
which was refered to from the tactic index.  We remove it so that
users find the other reference (which contains the deprecation
notice).

The changes to the doc of zarith are a follow-up to #11976.

3 files changed, 8 insertions, 18 deletions

diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 082ea4691b..e1b1ee8e8d 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -1,4 +1,4 @@
-.. _omega:
+.. _omega_chapter:
 
 Omega: a solver for quantifier-free problems in Presburger Arithmetic
 =====================================================================
@@ -28,6 +28,7 @@ Description of ``omega``
 ------------------------
 
 .. tacn:: omega
+   :name: omega
 
    .. deprecated:: 8.12
 
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 31fb1b7382..f72654b33b 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -55,7 +55,8 @@ __ 811Reals_
 Additionally, while the :tacn:`omega` tactic is not yet deprecated in
 this version of Coq, it should soon be the case and we already
 recommend users to switch to :tacn:`lia` in new proof scripts (see
-also the warning message in the :ref:`corresponding chapter <omega>`).
+also the warning message in the :ref:`corresponding chapter
+<omega_chapter>`).
 
 The ``dev/doc/critical-bugs`` file documents the known critical bugs
 of |Coq| and affected releases. See the `Changes in 8.11+beta1`_
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7da453b7af..1ecfa05f99 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4010,10 +4010,10 @@ At Coq startup, only the core database is nonempty and can be used.
 :arith: This database contains all lemmas about Peano’s arithmetic proved in the
         directories Init and Arith.
 
-:zarith: contains lemmas about binary signed integers from the directories
-         theories/ZArith. When required, the module Omega also extends the
-         database zarith with a high-cost hint that calls ``omega`` on equations
-         and inequalities in ``nat`` or ``Z``.
+:zarith: contains lemmas about binary signed integers from the
+         directories theories/ZArith. The database also contains
+         high-cost hints that call :tacn:`lia` on equations and
+         inequalities in ``nat`` or ``Z``.
 
 :bool: contains lemmas about booleans, mostly from directory theories/Bool.
 
@@ -4696,18 +4696,6 @@ Automating
       The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
       doesn't introduce variables into the context on its own.
 
-.. tacn:: omega
-   :name: omega
-
-   The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
-   procedure for Presburger arithmetic. It solves quantifier-free
-   formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities,
-   inequalities and disequalities on both the type :g:`nat` of natural numbers
-   and :g:`Z` of binary integers. This tactic must be loaded by the command
-   ``Require Import Omega``. See the additional documentation about omega
-   (see Chapter :ref:`omega`).
-
-
 .. tacn:: ring
    :name: ring