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

8 files changed, 31 insertions, 24 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6050fdc9a7..cf8707a469 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -404,7 +404,8 @@ module Hint_db = struct
       else rebuild_dn st (sl1', sl2', dn)
 
   let remove_list grs db =
-    let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
+    let filter (_, h) =
+      match h.name with PathHints [gr] -> not (List.mem gr grs) | _ -> true in
     let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in
     let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in
       { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
@@ -880,7 +881,7 @@ let interp_hints =
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
-  if List.mem "nocore" dbnames0 then
+  if String.List.mem "nocore" dbnames0 then
     error "The hint database \"nocore\" is meant to stay empty.";
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
   let env = Global.env() and sigma = Evd.empty in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9bc86a0b97..0864048f9f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -566,7 +566,7 @@ let find_positions env sigma t1 t2 =
           when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1)
             ->
 	  let sorts =
-            List.intersect Sorts.family_equal sorts (allowed_sorts env (fst sp1))
+            Sorts.List.intersect sorts (allowed_sorts env (fst sp1))
           in
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
@@ -577,7 +577,8 @@ let find_positions env sigma t1 t2 =
             List.flatten
 	      (List.map2_i (fun i -> findrec sorts ((sp1,i)::posn))
 		0 rargs1 rargs2)
-	  else if List.mem InType sorts then (* see build_discriminator *)
+	  else if Sorts.List.mem InType sorts
+          then (* see build_discriminator *)
 	    raise (DiscrFound (List.rev posn,sp1,sp2))
 	  else []
 
@@ -589,7 +590,9 @@ let find_positions env sigma t1 t2 =
           else
 	    let ty1_0 = get_type_of env sigma t1_0 in
 	    let s = get_sort_family_of env sigma ty1_0 in
-	    if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in
+	    if Sorts.List.mem s sorts
+            then [(List.rev posn,t1_0,t2_0)] else []
+  in
   try
     (* Rem: to allow injection on proofs objects, just add InProp *)
     Inr (findrec [InSet;InType] [] t1 t2)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 2a2a1e3560..19e7153b57 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -156,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let revargs,ownsign =
 	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
-             if List.mem id ivars then
+             if Id.List.mem id ivars then
 	       ((mkVar id)::revargs,add_named_decl d hyps)
 	     else
 	       (revargs,hyps))
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 3277393787..eb7b28690b 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -634,7 +634,9 @@ let eq_env x y = x == y
 let apply_rule by loccs : (hypinfo * int) pure_strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
-    if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
+    if nowhere_except_in
+    then Int.List.mem occ occs
+    else not (Int.List.mem occ occs) in
     fun (hypinfo, occ) env avoid t ty cstr evars ->
       let hypinfo =
         if not (eq_env hypinfo.cl.env env) then
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 06a9ab811c..aa254c2f86 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -64,7 +64,7 @@ let to_list v =
 end
 
 let is_variable env id =
-  List.mem id (Termops.ids_of_named_context (Environ.named_context env))
+  Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env))
 
 (* Transforms an id into a constr if possible, or fails with Not_found *)
 let constr_of_id env id =
@@ -155,7 +155,7 @@ let coerce_to_evaluable_ref env v =
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
-    if List.mem id (Termops.ids_of_context env) then EvalVarRef id
+    if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
   else
     let ev = match Value.to_constr v with
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 9e4060752b..6b06a05346 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -124,7 +124,7 @@ let lookup_ltacref r = KNmap.find r !mactab
 
 let find_ident id ist =
   Id.Set.mem id ist.ltacvars ||
-  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
+  Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars
 
@@ -138,7 +138,7 @@ let find_ctxvar id ist = Id.Set.mem id ist.ltacvars
 let find_ltacvar id ist = Id.Set.mem id ist.ltacvars
 
 let find_hyp id ist =
-  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
+  Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
 (* be fresh in which case it is binding later on *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 190c1ba58e..0e0ccac2e2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -289,7 +289,7 @@ let extend_values_with_bindings (ln,lm) lfun =
 (* Evaluation/interpretation *)
 
 let is_variable env id =
-  List.mem id (ids_of_named_context (Environ.named_context env))
+  Id.List.mem id (ids_of_named_context (Environ.named_context env))
 
 (* Debug reference *)
 let debug = ref DebugOff
@@ -472,7 +472,7 @@ let rec extract_ids ids lfun =
     let v = Value.normalize v in
     if has_type v (topwit wit_intro_pattern) then
       let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
-      if List.mem id ids then accu
+      if Id.List.mem id ids then accu
       else accu @ intropattern_ids (dloc, ipat)
     else accu
   in
@@ -910,7 +910,7 @@ let read_pattern lfun ist env sigma = function
 
 (* Reads the hypotheses of a Match Context rule *)
 let cons_and_check_name id l =
-  if List.mem id l then
+  if Id.List.mem id l then
     user_err_loc (dloc,"read_match_goal_hyps",
       strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
       " used twice in the same pattern."))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2505a43ad9..c1bd8e0c97 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1213,7 +1213,7 @@ let specialize mopt (c,lbind) g =
        tclEVARS clause.evd, term
   in
   match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with
-       | Var id when List.mem id (pf_ids_of_hyps g) ->
+       | Var id when Id.List.mem id (pf_ids_of_hyps g) ->
 	   tclTHEN tac
 	     (tclTHENFIRST
 	       (fun g -> internal_cut_replace id (pf_type_of g term) g)
@@ -1230,7 +1230,7 @@ let keep hyps gl =
   let ccl = pf_concl gl in
   let cl,_ =
     fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) ->
-      if List.mem hyp hyps
+      if Id.List.mem hyp hyps
         || List.exists (occur_var_in_decl env hyp) keep
 	|| occur_var env hyp ccl
       then (clear,decl::keep)
@@ -1572,7 +1572,7 @@ let simple_apply_in id c =
 
 let generalized_name c t ids cl = function
   | Name id as na ->
-      if List.mem id ids then
+      if Id.List.mem id ids then
 	errorlabstrm "" (pr_id id ++ str " is already used");
       na
   | Anonymous ->
@@ -1609,10 +1609,10 @@ let generalize_dep ?(with_let=false) c gl =
   let to_quantify = Context.fold_named_context seek sign ~init:[] in
   let to_quantify_rev = List.rev to_quantify in
   let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
-  let tothin = List.filter (fun id -> not (List.mem id init_ids)) qhyps in
+  let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | Var id when mem_named_context id sign && not (List.mem id init_ids)
+      | Var id when mem_named_context id sign && not (Id.List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -2199,13 +2199,14 @@ let cook_sign hyp0_opt indvars env =
          indvars too, so add it to indhyps. *)
       (if Option.is_empty hyp0_opt then indhyps := hyp::!indhyps);
       MoveFirst (* fake value *)
-    end else if List.mem hyp indvars then begin
+    end else if Id.List.mem hyp indvars then begin
       (* warning: hyp can still occur after induction *)
       (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *)
       indhyps := hyp::!indhyps;
       rhyp
     end else
-      if not (List.is_empty inhyps) && List.mem hyp inhyps || List.is_empty inhyps &&
+      if not (List.is_empty inhyps) && Id.List.mem hyp inhyps ||
+        List.is_empty inhyps &&
 	(List.exists (fun id -> occur_var_in_decl env id decl) allindhyps ||
          List.exists (fun (id,_,_) -> occur_var_in_decl env id decl) !decldeps)
       then begin
@@ -2222,11 +2223,11 @@ let cook_sign hyp0_opt indvars env =
   (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
   let compute_lstatus lhyp (hyp,_,_) =
     if Id.equal hyp hyp0 then raise (Shunt lhyp);
-    if List.mem hyp !ldeps then begin
+    if Id.List.mem hyp !ldeps then begin
       lstatus := (hyp,lhyp)::!lstatus;
       lhyp
     end else
-      if List.mem hyp !indhyps then lhyp else MoveAfter hyp
+      if Id.List.mem hyp !indhyps then lhyp else MoveAfter hyp
   in
   try
     let _ =
@@ -3156,7 +3157,7 @@ let clear_unselected_context id inhyps cls gl =
       match cls.onhyps with
       | Some hyps ->
 	  let to_erase (id',_,_ as d) =
-	    if List.mem id' inhyps then (* if selected, do not erase *) None
+	    if Id.List.mem id' inhyps then (* if selected, do not erase *) None
 	    else
 	      (* erase if not selected and dependent on id or selected hyps *)
 	      let test id = occur_var_in_decl (pf_env gl) id d in