aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index 5b6064fa9f..13761ca245 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -44,6 +44,10 @@ struct
| None -> true
| Some _ -> false
+ let is_valid_ident_part s = match Unicode.ident_refutation ("x"^s) with
+ | None -> true
+ | Some _ -> false
+
let of_bytes s =
let s = Bytes.to_string s in
check_valid s;