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

3 files changed, 13 insertions, 8 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 127d1d76e1..56a3701555 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -95,11 +95,16 @@ let interp_definition bl red_option c ctypopt =
 	let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
         let beq b1 b2 = if b1 then b2 else not b2 in
-        let impl_eq (x1, y1, z1) (x2, y2, z2) = beq x1 x2 && beq y1 y2 && beq z1 z2 in
-	(* Check that all implicit arguments inferable from the term is inferable from the type *)
-	if not (try List.for_all (fun (key,va) -> impl_eq (List.assoc key impsty) va) imps2 with Not_found -> false)
-	then msg_warning (strbrk "Implicit arguments declaration relies on type." ++
-		     spc () ++ strbrk "The term declares more implicits than the type here.");
+        let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in
+	(* Check that all implicit arguments inferable from the term
+           are inferable from the type *)
+        let chk (key,va) =
+          impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *)
+        in
+	if not (try List.for_all chk imps2 with Not_found -> false)
+	then msg_warning
+          (strbrk "Implicit arguments declaration relies on type." ++ spc () ++
+	   strbrk "The term declares more implicits than the type here.");
 	imps1@(Impargs.lift_implicits nb_args impsty),
         { const_entry_body = Future.from_val(body,Declareops.no_seff);
           const_entry_secctx = None;
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 45621ced8c..5846c73a85 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -149,7 +149,7 @@ let define_mutual_scheme_base kind suff f internal names mind =
   let cl, eff = f mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
-      try List.assoc i names
+      try List.assoc_f Int.equal i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let consts = Array.map2 (define internal) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0a21b6d6eb..b6e86a212c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -65,7 +65,7 @@ let evar_tactic = Store.field ()
 let subst_evar_constr evs n idf t = 
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
-  let evar_info id = List.assoc id evs in
+  let evar_info id = List.assoc_f Evar.equal id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
 	let { ev_name = (id, idstr) ;
@@ -425,7 +425,7 @@ let replace_appvars subst =
       if isVar f then
 	try
 	  let c' = List.map (map_constr aux) l in
-	  let (t, b) = List.assoc (destVar f) subst in
+	  let (t, b) = List.assoc_f Id.equal (destVar f) subst in
 	    mkApp (delayed_force hide_obligation, 
 		   [| prod_applist t c'; applistc b c' |])
 	with Not_found -> map_constr aux c