diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index ba997126e9..4b85faf8d3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -245,7 +245,7 @@ let check_required_module loc sc (ref,d) = try let _ = sp_of_global ref in () with Not_found -> user_err_loc (loc,"prim_token_interpreter", - str ("Cannot interpret numbers in "^sc^" without requiring first module " + str ("Cannot interpret in "^sc^" without requiring first module " ^(list_last d))) (* Look if some notation or numeral printer in [scope] can be used in |