More monomorphic List.mem + List.assoc + ...

 To reduce the amount of syntactic noise, we now provide
 a few inner modules Int.List, Id.List, String.List, Sorts.List
 which contain some monomorphic (or semi-monomorphic) functions
 such as mem, assoc, ...

 NB: for Int.List.mem and co we reuse List.memq and so on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 13 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 95aaf45184..8edb16850f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -766,7 +766,7 @@ let build_proof
 			}
 		      in
 		      build_proof_args do_finalize new_infos  g
-		  | Const c when not (List.mem c fnames) ->
+		  | Const c when not (List.mem_f Constant.equal c fnames) ->
 		      let new_infos =
 			{ dyn_infos with
 			    info = (f,args)
@@ -915,7 +915,7 @@ let generalize_non_dep hyp g =
   let hyp_typ = pf_type_of g (mkVar hyp) in
   let to_revert,_ =
     Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
-      if List.mem hyp hyps
+      if Id.List.mem hyp hyps
         || List.exists (Termops.occur_var_in_decl env hyp) keep
 	|| Termops.occur_var env hyp hyp_typ
 	|| Termops.is_section_variable hyp (* should be dangerous *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index cb9d12c5e4..e65ca94f06 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -367,7 +367,7 @@ let poseq_list_ids lcstr gl =
 let find_fapp (test:constr -> bool) g : fapp_info list =
   let pre_res = hdMatchSub (Tacmach.pf_concl g) test in
   let res =
-    List.fold_right (fun x acc -> if List.mem x acc then acc else x::acc) pre_res [] in
+    List.fold_right (List.add_set Pervasives.(=)) pre_res [] in
   (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res);
   res)
 
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 91ea714c16..dd02dfe8d1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -126,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if List.mem x_id (ids_of_binder bt)
+	if Id.List.mem x_id (ids_of_binder bt)
 	then l
 	else replace_var_by_term_in_binder x_id term l
 
@@ -134,14 +134,14 @@ let add_bt_names bt = List.append (ids_of_binder bt)
 
 let apply_args ctxt body args =
   let need_convert_id avoid id =
-    List.exists (is_free_in id) args || List.mem id avoid
+    List.exists (is_free_in id) args || Id.List.mem id avoid
   in
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
   let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
-       | Name id when List.mem id avoid ->
+       | Name id when Id.List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
 	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index a16b5f0fe5..79cba2c7c0 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -199,7 +199,7 @@ let rec alpha_pat excluded pat =
 	let new_id = Indfun_common.fresh_id excluded "_x" in
 	PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty
     | PatVar(loc,Name id) ->
-	if List.mem id excluded
+	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
@@ -208,7 +208,7 @@ let rec alpha_pat excluded pat =
     | PatCstr(loc,constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
-	    | Name id when List.mem id excluded ->
+	    | Name id when Id.List.mem id excluded ->
 		let new_id = Namegen.next_ident_away id excluded in
 		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
 	    | _ -> na,excluded,Id.Map.empty
@@ -412,7 +412,7 @@ let is_free_in id =
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (_,b,CastCoerce) -> is_free_in b
   and is_free_in_br (_,ids,_,rt) =
-    (not (List.mem id ids)) && is_free_in rt
+    (not (Id.List.mem id ids)) && is_free_in rt
   in
   is_free_in
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 57019b3fa5..a779680924 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -294,7 +294,9 @@ let check_not_nested forbidden e =
   let rec check_not_nested e =  
     match kind_of_term e with 
       | Rel _ -> ()
-      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x)
+      | Var x ->
+        if Id.List.mem x forbidden
+        then error ("check_not_nested : failure "^Id.to_string x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -652,7 +654,7 @@ let mkDestructEq :
   let to_revert =
     Util.List.map_filter
       (fun (id, _, t) ->
-        if List.mem id not_on_hyp || not (Termops.occur_term expr t)
+        if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t)
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
   let type_of_expr = pf_type_of g expr in