From 0a38eb0630cab142f3d470e561ddb5090055068a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 20 Apr 2020 16:46:48 +0200
Subject: [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.
---
 doc/sphinx/addendum/omega.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/addendum')

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
 
-- 
cgit v1.2.3