diff options
Diffstat (limited to 'kernel/names.ml')
| -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 e75900cfa..6ee96fddd 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ type identifier = string let id_ord = Pervasives.compare -let id_of_string s = check_ident s; String.copy s +let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id |