diff options
| author | herbelin | 2000-11-29 11:34:49 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-29 11:34:49 +0000 |
| commit | 88d05718d2e01680dc154e79e793c0d275677dab (patch) | |
| tree | 90d687d71f0e665ee45c41c1474e97b430e0b038 /lib | |
| parent | e63db2058943aa49c1b5f2d86d0fe3561ccc3da3 (diff) | |
Code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1017 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 7 |
1 files changed, 0 insertions, 7 deletions
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)] |
