diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/goptions.ml | 10 | ||||
| -rw-r--r-- | library/library.ml | 4 | ||||
| -rw-r--r-- | library/nametab.ml | 2 |
3 files changed, 7 insertions, 9 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 87c387080..7ceac2f6a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -60,7 +60,7 @@ module MakeTable = let nick = nickname A.key let _ = - if List.mem_assoc nick !A.table then + if String.List.mem_assoc nick !A.table then error "Sorry, this table name is already used." module MySet = Set.Make (struct type t = A.t let compare = compare end) @@ -121,7 +121,7 @@ module MakeTable = let string_table = ref [] -let get_string_table k = List.assoc_f String.equal (nickname k) !string_table +let get_string_table k = String.List.assoc (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_f String.equal (nickname k) !ref_table +let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig @@ -210,8 +210,8 @@ let check_key key = try let _ = get_option key in error "Sorry, this option name is already used." with Not_found -> - if List.mem_assoc (nickname key) !string_table - || List.mem_assoc (nickname key) !ref_table + if String.List.mem_assoc (nickname key) !string_table + || String.List.mem_assoc (nickname key) !ref_table then error "Sorry, this option name is already used." open Libobject diff --git a/library/library.ml b/library/library.ml index 09968c5ae..d2d67f484 100644 --- a/library/library.ml +++ b/library/library.ml @@ -234,9 +234,7 @@ let locate_qualified_library warn qid = 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_f String.equal lpath loadpath) base - in + let dir = add_dirpath_suffix (String.List.assoc 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 *) diff --git a/library/nametab.ml b/library/nametab.ml index fd27ef264..7eb48a714 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -240,7 +240,7 @@ let shortest_qualid ctx uname tab = let push_node node l = match node with - | Absolute (_,o) | Relative (_,o) when not (List.mem o l) -> o::l + | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l | _ -> l let rec flatten_idmap tab l = |