diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-31 10:45:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-31 10:45:10 +0000 |
| commit | c822d26db8d3fc5ad1b951ca2b7fe6131f5fe721 (patch) | |
| tree | 938b43b555e4cb44b306ff42935042504af7e160 /interp/notation.ml | |
| parent | 55b6884dda47f773156fa2484e927430c53b4e05 (diff) | |
Adaptation message d'erreur au cas des string
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7967 85f007b7-540e-0410-9357-904b9bb8a0f7
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 ba997126e..4b85faf8d 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 |