Removing now useless former fix to #3333 (check valid module names).

The fix is not anymore needed after Id.of_string was made strict
(5b218f87). This allows to support the whole official syntax of
identifiers and not just the alpha-numerical ones (without quote).

1 files changed, 0 insertions, 20 deletions

diff --git a/library/library.ml b/library/library.ml
index 28afa054e..1da2c591d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -620,25 +620,6 @@ let check_coq_overwriting p id =
       (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
-(* Verifies that a string starts by a letter and do not contain
-   others caracters than letters, digits, or `_` *)
-
-let check_module_name s =
-  let msg c =
-    strbrk "Invalid module name: " ++ str s ++ strbrk " character " ++
-    (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
-    strbrk " is not allowed in module names\n"
-  in
-  let err c = user_err  (msg c) in
-  match String.get s 0 with
-    | 'a' .. 'z' | 'A' .. 'Z' ->
-        for i = 1 to (String.length s)-1 do
-          match String.get s i with
-            | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '_'  -> ()
-            | c -> err c
-        done
-    | c -> err c
-
 let start_library fo =
   let ldir0 =
     try
@@ -648,7 +629,6 @@ let start_library fo =
   in
   let file = Filename.chop_extension (Filename.basename fo) in
   let id = Id.of_string file in
-  check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;