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.

3 files changed, 21 insertions, 8 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
diff --git a/interp/notation.ml b/interp/notation.ml
index 551f1bfa83..55ead946cb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -479,8 +479,11 @@ let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) =
 let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ?loc ~hdr:"prim_token_interpreter"
-    (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
+    match d with
+    | [] -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.")
+    | _ -> user_err ?loc ~hdr:"prim_token_interpreter"
+       (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 4a275de5b5..47ef381270 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -1,4 +1,3 @@
-
 (* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *)
 
 (* https://github.com/coq/coq/pull/8064#discussion_r202497516 *)
@@ -290,15 +289,14 @@ Module Test16.
     Inductive Foo := foo (_ : a.T).
     Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O.
     Definition of_uint (x : Decimal.uint) : Foo := foo a.t.
-    Numeral Notation Foo of_uint to_uint : test16_scope.
-    Check let v := 0%test16 in v : Foo. (* Prints wrong: let v := foo a.t in v : Foo *)
+    Global Numeral Notation Foo of_uint to_uint : test16_scope.
+    Check let v := 0%test16 in v : Foo.
   End F.
   Module a <: A.
     Definition T : Set := unit.
     Definition t : T := tt.
   End a.
   Module Import f := F a.
-  (* Check let v := 0%test16 in v : Foo. *)
-  (* Error: Anomaly "Uncaught exception Failure("List.last")."
-Please report at http://coq.inria.fr/bugs/. *)
+  (** Ideally this should work, but it should definitely not anomaly *)
+  Fail Check let v := 0%test16 in v : Foo.
 End Test16.