Merge PR #12149: Fix documentation following #12038.

Reviewed-by: SkySkimmer

3 files changed, 37 insertions, 17 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.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5034d9a3c9..700170b3c6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -906,14 +906,14 @@ command: [
 | DELETE "Unset" option_table
 | REPLACE "Set" option_table option_setting
 | WITH OPT "Export" "Set" option_table   (* set flag *)
-| REPLACE "Test" option_table "for" LIST1 option_ref_value
-| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| REPLACE "Test" option_table "for" LIST1 table_value
+| WITH "Test" option_table OPT ( "for" LIST1 table_value )
 | DELETE "Test" option_table
 
 (* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Add" IDENT IDENT LIST1 option_ref_value
-| WITH "Add" option_table LIST1 option_ref_value
-| DELETE "Add" IDENT LIST1 option_ref_value
+| REPLACE "Add" IDENT IDENT LIST1 table_value
+| WITH "Add" option_table LIST1 table_value
+| DELETE "Add" IDENT LIST1 table_value
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
@@ -969,9 +969,9 @@ command: [
 | DELETE "Preterm"
 
 (* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value
-| WITH "Remove" option_table LIST1 option_ref_value
-| DELETE "Remove" IDENT LIST1 option_ref_value
+| REPLACE "Remove" IDENT IDENT LIST1 table_value
+| WITH "Remove" option_table LIST1 table_value
+| DELETE "Remove" IDENT LIST1 table_value
 | DELETE "Restore" "State" IDENT
 | DELETE "Restore" "State" ne_string
 | "Restore" "State" [ IDENT | ne_string ]
@@ -1550,7 +1550,7 @@ SPLICE: [
 | constructor_type
 | record_binder
 | at_level_opt
-| option_ref_value
+| table_value
 | positive_search_mark
 | in_or_out_modules
 | option_setting
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 04c20a7203..4274dccb40 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -524,12 +524,12 @@ command: [
 | "Set" option_table option_setting
 | "Unset" option_table
 | "Print" "Table" option_table
-| "Add" IDENT IDENT LIST1 option_ref_value
-| "Add" IDENT LIST1 option_ref_value
-| "Test" option_table "for" LIST1 option_ref_value
+| "Add" IDENT IDENT LIST1 table_value
+| "Add" IDENT LIST1 table_value
+| "Test" option_table "for" LIST1 table_value
 | "Test" option_table
-| "Remove" IDENT IDENT LIST1 option_ref_value
-| "Remove" IDENT LIST1 option_ref_value
+| "Remove" IDENT IDENT LIST1 table_value
+| "Remove" IDENT LIST1 table_value
 | "Write" "State" IDENT
 | "Write" "State" ne_string
 | "Restore" "State" IDENT
@@ -1318,7 +1318,7 @@ option_setting: [
 | STRING
 ]
 
-option_ref_value: [
+table_value: [
 | global
 | STRING
 ]