Merge PR#646: Revised behavior on ill-formed identifiers

1 files changed, 5 insertions, 13 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 811b4a62a5..f5b3f4e007 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,16 +34,8 @@ struct
 
   let hash = String.hash
 
-  let warn_invalid_identifier =
-    CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
-                     ~default:CWarnings.Disabled
-                     (fun s -> str s)
-
-  let check_soft ?(warn = true) x =
-    let iter (fatal, x) =
-      if fatal then CErrors.error x else
-        if warn then warn_invalid_identifier x
-    in
+  let check_valid ?(strict=true) x =
+    let iter (fatal, x) = if fatal || strict then CErrors.error x in
     Option.iter iter (Unicode.ident_refutation x)
 
   let is_valid s = match Unicode.ident_refutation s with
@@ -52,15 +44,15 @@ struct
 
   let of_bytes s =
     let s = Bytes.to_string s in
-    check_soft s;
+    check_valid s;
     String.hcons s
 
   let of_string s =
-    let () = check_soft s in
+    let () = check_valid s in
     String.hcons s
 
   let of_string_soft s =
-    let () = check_soft ~warn:false s in
+    let () = check_valid ~strict:false s in
     String.hcons s
 
   let to_string id = id