diff options
| author | Jason Gross | 2018-08-31 17:01:43 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:55 -0400 |
| commit | 17cb475550a0f4efe9f3f4c58fdbd9039f5fdd68 (patch) | |
| tree | 7a9ef8ae3a878dd1e29a176d45c552da006379fb /interp | |
| parent | 31d58c9ee979699e733a561ec4eef6b0829fe73a (diff) | |
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.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 *) |