From df452a678d4fcb82a35847a194408e1e59846ad0 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 31 Dec 2019 12:54:03 +0100
Subject: [refman] [changelog] Announce omega replacement.

---
 doc/sphinx/changes.rst | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/sphinx/changes.rst')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 1d0c937792..d7a582c3e2 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -50,6 +50,11 @@ __ 811RefineInstance_
 __ 811SSRUnderOver_
 __ 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>`).
+
 The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq|
 and affected releases. See the `Changes in 8.11+beta1`_ section for the
 detailed list of changes, including potentially breaking changes marked with
-- 
cgit v1.2.3