Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr"

Reviewed-by: herbelin
Ack-by: Zimmi48

4 files changed, 9 insertions, 9 deletions

diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
new file mode 100644
index 0000000000..0ab9a58e6f
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Drop prefixes from grammar non-terminal names,
+  e.g. "constr:global" -> "global", "Prim.name" -> "name".
+  Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`.
+  (`#13096 <https://github.com/coq/coq/pull/13096>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6ba53b581b..5148fa84c9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -429,10 +429,6 @@ Displaying information about notations
    productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
    and `tactic_then_gen` which are not shown and can't be printed.
 
-   The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify
-   what part of the grammar a nonterminal is from.  If you examine nonterminal definitions
-   in the source code, they are identified only by the name following the colon.
-
    Most of the grammar in the documentation was updated in 8.12 to make it accurate and
    readable.  This was done using a new developer tool that extracts the grammar from the
    source code, edits it and inserts it into the documentation files.  While the
@@ -467,11 +463,11 @@ Displaying information about notations
    `tactic_expr`, designated as "5", "4" and "3".  Level 3 is right-associative,
    which applies to the productions within it, such as the `try` construct::
 
-     Entry tactic:tactic_expr is
+     Entry tactic_expr is
      [ "5" RIGHTA
-       [ tactic:binder_tactic ]
+       [ binder_tactic ]
      | "4" LEFTA
-       [ SELF; ";"; tactic:binder_tactic
+       [ SELF; ";"; binder_tactic
        | SELF; ";"; SELF
        | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
      | "3" RIGHTA
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..328175e65c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1761,7 +1761,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..6ae99880b3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1268,7 +1268,6 @@ int_or_id: [
 ]
 
 language: [
-| "Ocaml"      (* extraction plugin *)
 | "OCaml"      (* extraction plugin *)
 | "Haskell"      (* extraction plugin *)
 | "Scheme"      (* extraction plugin *)