From a3a5711d8c2f9f0e12ed707c8b69c828e30bbcf4 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 24 Oct 2013 09:41:19 +0000
Subject: 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
---
 library/goptions.ml | 4 ++--
 library/impargs.ml  | 5 +++--
 library/library.ml  | 9 ++++++---
 3 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'library')

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
-- 
cgit v1.2.3