diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index b79a526083..b3a4ccba51 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -106,7 +106,7 @@ let check_ident_suffix i l s = let c = String.get s i in if not (is_letter c or is_digit c or c = '\'' or c = '_' or c = '@') then error - ("Character "^(String.sub s i 1)^" is not allowed in an identifier") + ("Character "^(String.sub s i 1)^" is not allowed in identifier "^s) done let check_ident s = |