Give a proper error message on num-not in functor

Numeral Notations are not well-supported inside functors.  We now give a
proper error message rather than an anomaly when this occurs.

1 files changed, 12 insertions, 0 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 886ca0472a..b46382dbbf 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1462,6 +1462,18 @@ Numeral notations
     concrete numeral expressed as a decimal.  They may not return
     opaque constants.
 
+  .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment.
+
+    The inductive type used to register the numeral notation is no
+    longer available in the environment.  Most likely, this is because
+    the numeral notation was declared inside a functor for an
+    inductive type inside the functor.  This use case is not currently
+    supported.
+
+    Alternatively, you might be trying to use a primitive token
+    notation from a plugin which forgot to specify which module you
+    must :g:`Require` for access to that notation.
+
   .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]).
 
     The type passed to :cmd:`Numeral Notation` must be a single