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

9 files changed, 22 insertions, 22 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index be62e65b3..d10a52fce 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -496,7 +496,7 @@ let extract_rhs pb =
 let occur_in_rhs na rhs =
   match na with
     | Anonymous -> false
-    | Name id -> List.mem id rhs.rhs_vars
+    | Name id -> Id.List.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn = function
   | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
@@ -1521,7 +1521,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
       let depvl = free_rels ty in
       let inst =
 	List.map_i
-	  (fun i _ -> if List.mem i vl then u else mkRel i) 1
+	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
       let rel_filter =
 	List.map (fun a -> not (isRel a) || dependent a u
@@ -1760,7 +1760,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c =
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = List.assoc_f Int.equal (n - lift) subst in
+	      let idx = Int.List.assoc (n - lift) subst in
 		mkRel (idx + lift)
 	    with Not_found ->
 	      (* A variable that is not matched, lift over the arsign. *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aa8f2d08e..63d7b6294 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1179,8 +1179,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
           let ts = expansions_of_var aliases t in
-          (** FIXME : [List.mem] on constr ???*)
-          let test c = isEvar c || List.mem c ts in
+          let test c = isEvar c || List.mem_f Constr.equal c ts in
           let filter = restrict_upon_filter evd evk test argsv' in
           let filter = closure_of_filter evd evk' filter in
           let candidates = extract_candidates sols in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 88702b350..94ff780ec 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -139,7 +139,7 @@ let occur_glob_constr id =
 	|| (List.exists occur_pattern pl)
     | GLetTuple (loc,nal,rtntyp,b,c) ->
 	occur_return_type rtntyp id
-        || (occur b) || (not (List.mem (Name id) nal) && (occur c))
+        || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
     | GIf (loc,c,rtntyp,b1,b2) ->
 	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
     | GRec (loc,fk,idl,bl,tyl,bv) ->
@@ -158,7 +158,7 @@ let occur_glob_constr id =
       | CastVM t | CastNative t -> occur t | CastCoerce -> false)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
 
-  and occur_pattern (loc,idl,p,c) = not (List.mem id idl) && (occur c)
+  and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
 
   and occur_option = function None -> false | Some p -> occur p
 
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 23996282c..bf9fd8a10 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -55,7 +55,7 @@ let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
     mib.mind_params_ctxt
   in
 
-  if not (List.mem kind (elim_sorts specif)) then
+  if not (Sorts.List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
 	 (NotAllowedCaseAnalysis (false, Termops.new_sort_in_family kind, ind)));
@@ -508,10 +508,10 @@ let check_arities listdepkind =
   let _ = List.fold_left
     (fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
        let kelim = elim_sorts (mibi,mipi) in
-       if not (List.exists ((==) kind) kelim) then raise
+       if not (Sorts.List.mem kind kelim) then raise
 	 (RecursionSchemeError
 	   (NotAllowedCaseAnalysis (true, Termops.new_sort_in_family kind,mind)))
-       else if List.mem ni ln then raise
+       else if Int.List.mem ni ln then raise
 	 (RecursionSchemeError (NotMutualInScheme (mind,mind)))
        else ni::ln)
 	    [] listdepkind
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b0637a972..812900ea8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -79,7 +79,7 @@ let mis_is_recursive_subset listind rarg =
     List.exists
       (fun ra ->
         match dest_recarg ra with
-	  | Mrec (_,i) -> List.mem i listind
+	  | Mrec (_,i) -> Int.List.mem i listind
           | _ -> false) rvec
   in
   Array.exists one_is_rec (dest_subterms rarg)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 22f154795..3bbd8af44 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -27,8 +27,8 @@ let convert_occs = function
 
 let is_selected occ = function
   | AllOccurrences -> true
-  | AllOccurrencesBut l -> not (List.mem occ l)
-  | OnlyOccurrences l -> List.mem occ l
+  | AllOccurrencesBut l -> not (Int.List.mem occ l)
+  | OnlyOccurrences l -> Int.List.mem occ l
   | NoOccurrences -> false
 
 (** Usual clauses *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 13eb91393..b8dbefb88 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -183,7 +183,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   if not (List.distinct_f Int.compare reversible_rels) then
     raise Elimconst;
   List.iteri (fun i t_i ->
-    if not (List.mem_assoc (i+1) li) then
+    if not (Int.List.mem_assoc (i+1) li) then
       let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in
       match List.intersect Int.equal fvs reversible_rels with
       | [] -> ()
@@ -888,8 +888,8 @@ let contextually byhead (occs,c) f env sigma t =
     try
       let subst = if byhead then matches_head c t else matches c t in
       let ok =
-	if nowhere_except_in then List.mem !pos locs
-	else not (List.mem !pos locs) in
+	if nowhere_except_in then Int.List.mem !pos locs
+	else not (Int.List.mem !pos locs) in
       incr pos;
       if ok then
         let subst' = Id.Map.map (traverse envc) subst in
@@ -923,8 +923,8 @@ let substlin env evalref n (nowhere_except_in,locs) c =
     if nowhere_except_in && !pos > maxocc then c
     else if eq_constr c term then
       let ok =
-	if nowhere_except_in then List.mem !pos locs
-	else not (List.mem !pos locs) in
+	if nowhere_except_in then Int.List.mem !pos locs
+	else not (Int.List.mem !pos locs) in
       incr pos;
       if ok then value else c
     else
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9ecf86698..5fb74dcad 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -625,7 +625,7 @@ type meta_value_map = (metavariable * constr) list
 
 let rec subst_meta bl c =
   match kind_of_term c with
-    | Meta i -> (try List.assoc_f Int.equal i bl with Not_found -> c)
+    | Meta i -> (try Int.List.assoc i bl with Not_found -> c)
     | _ -> map_constr (subst_meta bl) c
 
 (* First utilities for avoiding telescope computation for subst_term *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 9fe95a119..bbcc5727b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -79,8 +79,8 @@ let e_check_branch_types env evdref ind cj (lfj,explft) =
   done
 
 let max_sort l =
-  if List.mem InType l then InType else
-  if List.mem InSet l then InSet else InProp
+  if Sorts.List.mem InType l then InType else
+  if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
@@ -93,7 +93,8 @@ let e_is_correct_arity env evdref c pj ind specif params =
         if not (Evarconv.e_cumul env evdref a1 a1') then error ();
         srec (push_rel (na1,None,a1) env) t ar'
     | Sort s, [] ->
-        if not (List.mem (family_of_sort s) allowed_sorts) then error ()
+        if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
+        then error ()
     | Evar (ev,_), [] ->
         let s = Termops.new_sort_in_family (max_sort allowed_sorts) in
         evdref := Evd.define ev (mkSort s) !evdref