diff options
| author | letouzey | 2013-10-24 09:41:19 +0000 |
|---|---|---|
| committer | letouzey | 2013-10-24 09:41:19 +0000 |
| commit | a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 (patch) | |
| tree | 02972edf2946cbb9f4a30133d9f66dd5cdbe7987 /library/library.ml | |
| parent | bb5e6d7c39211349d460db0b61b2caf3d099d5b6 (diff) | |
Turn many List.assoc into List.assoc_f
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/library/library.ml b/library/library.ml index a15b66d200..09968c5aea 100644 --- a/library/library.ml +++ b/library/library.ml @@ -232,8 +232,11 @@ let locate_qualified_library warn qid = let loadpath = Loadpath.expand_path dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let name = Id.to_string base ^ ".vo" in - let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in + let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name + in + let dir = + add_dirpath_suffix (List.assoc_f String.equal lpath loadpath) base + in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -382,7 +385,7 @@ let rec intern_library needed (dir, f) = try find_library dir, needed with Not_found -> (* Look if already listed and consequently its dependencies too *) - try List.assoc dir needed, needed + try List.assoc_f DirPath.equal dir needed, needed with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in |