Update numeral notation printing doc

Fixes #9844

1 files changed, 7 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index b5e91b17e6..2765661749 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -626,7 +626,13 @@ exception NotAValidPrimToken
 
 (** The uninterp function below work at the level of [glob_constr]
     which is too low for us here. So here's a crude conversion back
-    to [constr] for the subset that concerns us. *)
+    to [constr] for the subset that concerns us.
+
+    Note that if you update [constr_of_glob], you should update the
+    corresponding numeral notation *and* string notation doc in
+    doc/sphinx/user-extensions/syntax-extensions.rst that describes
+    what it means for a term to be ground / to be able to be
+    considered for parsing. *)
 
 let rec constr_of_glob env sigma g = match DAst.get g with
   | Glob_term.GRef (ConstructRef c, _) ->