From 88d05718d2e01680dc154e79e793c0d275677dab Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 Nov 2000 11:34:49 +0000
Subject: Code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1017 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index 05b147cee3..429c1666e0 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -32,12 +32,6 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
-let check_is_ident s =
-  let len = String.length s in
-  if len = 0 then invalid_arg "parse_loadpath: is not a valid name";
-  (* TODO... *)
-  ()
-
 let parse_loadpath s =
   let len = String.length s in
   let rec decoupe_dirs n =
@@ -46,7 +40,6 @@ let parse_loadpath s =
       if pos = n then
 	invalid_arg "parse_loadpath: find an empty dir in loadpath";
       let dir = String.sub s n (pos-n) in
-      check_is_ident dir;
       dir :: (decoupe_dirs (succ pos))
     with
       | Not_found -> [String.sub s n (len-n)]
-- 
cgit v1.2.3