diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 09:41:19 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 09:41:19 +0000 |
| commit | a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 (patch) | |
| tree | 02972edf2946cbb9f4a30133d9f66dd5cdbe7987 /library | |
| 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')
| -rw-r--r-- | library/goptions.ml | 4 | ||||
| -rw-r--r-- | library/impargs.ml | 5 | ||||
| -rw-r--r-- | library/library.ml | 9 |
3 files changed, 11 insertions, 7 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index d38d2762a..87c387080 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -121,7 +121,7 @@ module MakeTable = let string_table = ref [] -let get_string_table k = List.assoc (nickname k) !string_table +let get_string_table k = List.assoc_f String.equal (nickname k) !string_table module type StringConvertArg = sig @@ -150,7 +150,7 @@ module MakeStringTable = let ref_table = ref [] -let get_ref_table k = List.assoc (nickname k) !ref_table +let get_ref_table k = List.assoc_f String.equal (nickname k) !ref_table module type RefConvertArg = sig diff --git a/library/impargs.ml b/library/impargs.ml index 66900ee42..61ea7a87a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -352,8 +352,9 @@ let set_manual_implicits env flags enriching autoimps l = | (Name id,imp)::imps -> let l',imp,m = try - let (b, fi, fo) = List.assoc (ExplByName id) l in - List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi)) + let eq = (Pervasives.(=) : explicitation -> explicitation -> bool) in (* FIXME *) + let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in + List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) with Not_found -> try let (id, (b, fi, fo)), l' = assoc_by_pos k l in diff --git a/library/library.ml b/library/library.ml index a15b66d20..09968c5ae 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 |