diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 4 |
4 files changed, 10 insertions, 18 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d03a31c044..3b9760f586 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -112,11 +112,11 @@ and checked to be :math:`-1`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` -tactics. Roughly speaking, the deductive power of lia is the combined deductive -power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear -goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following -so-called *omega nightmare* :cite:`TheOmegaPaper`. + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and -:tacn:`romega` is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 828505b850..03d4f148e3 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -23,13 +23,6 @@ Description of ``omega`` If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -.. tacv:: romega - :name: romega - - .. deprecated:: 8.9 - - Use :tacn:`lia` instead. - Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index daf34500bf..593afa8f20 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -522,7 +522,7 @@ The Vernacular ============== .. productionlist:: coq - decorated-sentence : [`decoration`] `sentence` + decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -1438,7 +1438,7 @@ Attributes Any vernacular command can be decorated with a list of attributes, enclosed between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) -and separated by commas ``,``. +and separated by commas ``,``. Multiple space-separated blocks may be provided. Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 837d3f10a2..be65ff7570 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -35,7 +35,7 @@ Displaying .. cmdv:: Print {? Term } @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: About @qualid @@ -49,7 +49,7 @@ Displaying .. cmdv:: About @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: Print All |