diff options
Diffstat (limited to 'interp/notation.ml')
| -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 *) |