diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index dd74e192f..50f28b020 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -58,14 +58,14 @@ let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p) let parse_dir s = let len = String.length s in let rec decoupe_dirs dirs n = - if Int.equal n len && n > 0 then error (s ^ " is an invalid path."); + if Int.equal n len && n > 0 then user_err Pp.(str @@ s ^ " is an invalid path."); if n >= len then dirs else let pos = try String.index_from s n '.' with Not_found -> len in - if Int.equal pos n then error (s ^ " is an invalid path."); + if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path."); let dir = String.sub s n (pos-n) in decoupe_dirs ((Id.of_string dir)::dirs) (pos+1) in |