diff options
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 |
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 ff2b742220..6615b98660 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 a969bf5482..7e6da490fb 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3952,10 +3952,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. @@ -4602,18 +4602,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 |