diff options
| author | Pierre-Marie Pédrot | 2020-01-11 14:51:42 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-11 14:51:42 +0100 |
| commit | 8a5e3cd84ab077f0bbe57bd13dca750cda043bf4 (patch) | |
| tree | 4cdd45e5a6f009747a27b179f5a97de7cfc41fbf /doc/sphinx/changes.rst | |
| parent | ba6ea757c79318a452bc1c044e140ebade6b224c (diff) | |
| parent | df452a678d4fcb82a35847a194408e1e59846ad0 (diff) | |
Merge PR #11349: [refman] [changelog] Announce omega replacement.
Ack-by: ejgallego
Reviewed-by: maximedenes
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 |