From 73c924d3d4bcc22a179cb974603f9072599ebb77 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 15:35:21 -0400
Subject: Update numeral notation printing doc

Fixes #9844
---
 interp/notation.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'interp')

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, _) ->
-- 
cgit v1.2.3