diff options
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 33fc211fa5..21000889d3 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 |