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

11 files changed, 23 insertions, 18 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 8060dcabf..01f90f6c6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -278,7 +278,8 @@ let rec bind_primary_aliases map pat =
 	  List.fold_left bind_primary_aliases map1 lpat
 
 let bind_secondary_aliases map subst =
-  Id.Map.fold (fun ids (idp : Id.t) map -> (ids,List.assoc idp map)::map) subst map
+  Id.Map.fold
+    (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map
 
 let bind_aliases patvars subst patt =
   let map = bind_primary_aliases [] patt in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e18df6e46..673b749e1 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1189,7 +1189,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls
     | End_patt (id,(nparams,nhyps)),[] -> 
 	begin
-	  match List.assoc id args with
+	  match List.assoc_f Id.equal id args with
 	      [None,br_args] -> 
 		let all_metas = 
 		  List.init (nparams + nhyps) (fun n -> mkMeta (succ n))  in
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 45977b657..e6bcefe22 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -213,7 +213,7 @@ let get_decl_in_structure r struc =
   try
     let base_mp,ll = labels_of_ref r in
     if not (at_toplevel base_mp) then error_not_visible r;
-    let sel = List.assoc base_mp struc in
+    let sel = List.assoc_f ModPath.equal base_mp struc in
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index eeaf270c3..083108bef 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -32,7 +32,7 @@ let unif t1 t2=
     match kind_of_term t with
 	Meta i->
 	  (try
-	     head_reduce (List.assoc i !sigma)
+	     head_reduce (List.assoc_f Int.equal i !sigma)
 	   with Not_found->t)
       | _->t in
     Queue.add (t1,t2) bige;
@@ -105,7 +105,7 @@ let mk_rel_inst t=
     match kind_of_term t with
 	Meta n->
 	  (try
-	     mkRel (d+(List.assoc n !rel_env))
+	     mkRel (d+(List.assoc_f Int.equal n !rel_env))
 	   with Not_found->
 	     let m= !new_rel in
 	       incr new_rel;
@@ -117,7 +117,7 @@ let mk_rel_inst t=
 
 let unif_atoms i dom t1 t2=
   try
-    let t=List.assoc i (unif t1 t2) in
+    let t=List.assoc_f Int.equal i (unif t1 t2) in
       if isMeta t then Some (Phantom dom)
       else Some (Real(mk_rel_inst t,value i t1))
   with
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 58f43ed49..e5d8fe4c1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -482,7 +482,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
     List.map
-      (function const -> List.assoc const this_block_funs_indexes)
+      (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes)
       funs
   in
   let ind_list =
@@ -665,7 +665,7 @@ let build_case_scheme fa =
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc (destConst funs) this_block_funs_indexes
+    List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes
   in
   let ind_fun =
 	 let ind = first_fun_kn,funs_indexes in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 96a60424c..57019b3fa 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -701,7 +701,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
     args;
   begin
     try 
-      let v = List.assoc args expr_info.args_assoc in 
+      let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in 
       tclTHENLIST[
 	continuation_tac new_infos;
@@ -951,7 +951,7 @@ let equation_app f_and_args expr_info continuation_tac infos =
 let equation_app_rec (f,args) expr_info continuation_tac info = 
   begin
     try
-      let v = List.assoc args expr_info.args_assoc in
+      let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in
       let new_infos = {expr_info with info = v} in
       observe_tac (str "app_rec found") (continuation_tac new_infos)
     with Not_found ->
diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml
index eb3d81901..c8957f4cd 100644
--- a/plugins/micromega/sos.ml
+++ b/plugins/micromega/sos.ml
@@ -1377,7 +1377,7 @@ let allvarorders l =
   List.map (fun vlis x -> index x vlis) (allpermutations l);;
 
 let changevariables_monomial zoln (m:monomial) =
-  foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;;
+  foldl (fun a x k -> (List.assoc_f (=) x zoln |-> k) a) monomial_1 m;;
 
 let changevariables zoln pol =
   foldl (fun a m c -> (changevariables_monomial zoln m |-> c) a)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c39b2ff0a..5c057231a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -131,20 +131,24 @@ let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 
 let rev_assoc k =
   let rec loop = function
-    | [] -> raise Not_found | (v,k')::_ when Int.equal k k' -> v | _ :: l -> loop l
+    | [] -> raise Not_found
+    | (v,k')::_ when Int.equal k k' -> v
+    | _ :: l -> loop l
   in
   loop
 
 let tag_hypothesis,tag_of_hyp, hyp_of_tag =
   let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
-  (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
+  (fun h ->
+    try List.assoc_f Id.equal h !l with Not_found -> failwith "tag_hypothesis"),
   (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
 
 let hide_constr,find_constr,clear_tables,dump_tables =
   let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
-  (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
+  (fun h ->
+    try List.assoc_f Constr.equal h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
   (fun () -> !l)
 
@@ -1018,7 +1022,7 @@ let replay_history tactic_normalisation =
 	  begin
 	    try
 	      tclTHEN
-		(List.assoc (hyp_of_tag e.id) tactic_normalisation)
+		(List.assoc_f Id.equal (hyp_of_tag e.id) tactic_normalisation)
 		(loop l)
 	    with Not_found -> loop l end
       | NEGATE_CONTRADICT (e2,e1,b) :: l ->
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index cf1a7e6db..b74faf30b 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system =
         let s2' = List.map remove_int s2 in
         let (r1,relie1) = solve s1'
 	and (r2,relie2) = solve s2' in
-	let (eq,id1,id2) = List.assoc id explode_map in
+	let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in
 	[SPLIT_INEQ(eq,(id1,r1),(id2, r2))],
         eq.id :: Util.List.union Int.equal relie1 relie2
       with FULL_SOLUTION (x0,x1) -> (x0,x1)
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 860a2524c..c5a0f798c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -198,7 +198,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i
    le terme d'un monome (le plus souvent un atome) *)
 
 let intern_omega env t =
-  begin try List.assoc t env.om_vars
+  begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *)
   with Not_found ->
     let v = new_omega_var () in
     env.om_vars <- (t,v) :: env.om_vars; v
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index f98625b64..26fab4ac2 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -188,7 +188,7 @@ let typeur sigma metamap =
   let rec type_of env cstr=
     match Term.kind_of_term cstr with
     | T.Meta n ->
-          (try T.strip_outer_cast (List.assoc n metamap)
+          (try T.strip_outer_cast (Util.List.assoc_f Int.equal n metamap)
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in