diff options
| author | Gaëtan Gilbert | 2020-04-21 19:28:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-21 19:28:06 +0200 |
| commit | d91f294454ccc0056eb8ca5a95cb1b002724ebc6 (patch) | |
| tree | 969879cf2021e14e10a16cfc657d0db2b26549a3 /doc/sphinx | |
| parent | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (diff) | |
| parent | f38af4f2a04fe11802c4ff17234a27a590953fe2 (diff) | |
Merge PR #12149: Fix documentation following #12038.
Reviewed-by: SkySkimmer
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7d031b9b7a..a0d1080314 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,9 +91,15 @@ capital letter. This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. They are described :ref:`here <set_unset_scope_qualifiers>`. - .. warn:: There is no option @setting_name. + .. warn:: There is no flag or option with this name: "@setting_name". - This message also appears for unknown flags. + This warning message can be raised by :cmd:`Set` and + :cmd:`Unset` when :n:`@setting_name` is unknown. It is a + warning rather than an error because this helps library authors + produce Coq code that is compatible with several Coq versions. + To preserve the same behavior, they may need to set some + compatibility flags or options that did not exist in previous + Coq versions. .. cmd:: Unset @setting_name :name: Unset @@ -119,6 +125,20 @@ capital letter. whether the table contains each specified value, otherise this is equivalent to :cmd:`Print Table`. The `for` clause is not valid for flags and options. + .. exn:: There is no flag, option or table with this name: "@setting_name". + + This error message is raised when calling the :cmd:`Test` + command (without the `for` clause), or the :cmd:`Print Table` + command, for an unknown :n:`@setting_name`. + + .. exn:: There is no qualid-valued table with this name: "@setting_name". + There is no string-valued table with this name: "@setting_name". + + These error messages are raised when calling the :cmd:`Add` or + :cmd:`Remove` commands, or the :cmd:`Test` command with the + `for` clause, if :n:`@setting_name` is unknown or does not have + the right type. + .. cmd:: Print Options Prints the current value of all flags and options, and the names of all tables. |