From 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 17:01:43 -0400
Subject: 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.
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'doc/sphinx')

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