Document the fact that a %public symbol can now be split, even inside a single .mly file.

CHANGES.md

@@ -20,6 +20,10 @@
   ignored by Menhir's back-ends, but are written to `.cmly` files, thus
   can be exploited by external tools via MenhirSdk. (Suggested by Frédéric Bour.)
 
+* The definition of a %public nonterminal symbol can now be split into several
+  parts within a single .mly file. (This used to be permitted only over
+  multiple .mly files.) (Suggested by Frédéric Bour.)
+
 * Improved the syntax error message that is displayed when a `.mly` file
   is incorrect: the previous and next token are shown.
 

TODO

 * Document the recent additions (CHANGES + doc).
-  - ability to split a %public symbol, even within a single unit
   - menhirLib: new functions
       loop_handle_undo, shifts, acceptable
       find_default_reduction

doc/main.tex

@@ -794,10 +794,11 @@ public, that is, if either its definition carries the keyword \dpublic or
 $N$ is declared to be a start symbol. A public nonterminal symbol is never
 renamed, so it can be referred to by modules other than its defining module.
 
-In fact, it is even permitted to split the definition of a public nonterminal
-symbol over multiple modules. That is, a public nonterminal symbol $N$ can
-have multiple definitions in distinct modules. When the modules are joined,
-the definitions are joined as well, using the choice (\barre) operator. This
+In fact, it is permitted to split the definition of a \emph{public} nonterminal
+symbol, over multiple modules and/or within a single module.
+That is, a public nonterminal symbol $N$ can
+have multiple definitions, within one module and/or in distinct modules.
+All of these definitions are joined using the choice (\barre) operator. This
 feature allows splitting a grammar specification in a manner that is
 independent of the grammar's structure. For instance, in the grammar of a
 programming language, the definition of the nonterminal symbol \nt{expression}