Some documentation and cleaning of CList and Util interfaces.

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

5 files changed, 12 insertions, 10 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0ece3496e1..98cc42aaf5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -912,7 +912,7 @@ let adjust_impossible_cases pb pred tomatch submat =
       (* we add an "assert false" case *)
       let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in
       let aliasnames =
-	map_succeed (function Alias _ | NonDepAlias -> Anonymous | _ -> failwith"") tomatch
+	List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch
       in
       [ { patterns = pats;
           rhs = { rhs_env = pb.env;
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 700b168ae1..af3227729e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1120,7 +1120,7 @@ let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_e
       res
 
 let effective_projections =
-  map_succeed (function Invertible c -> c | _ -> failwith"")
+  List.map_filter (function Invertible c -> Some c | _ -> None)
 
 let instance_of_projection f env t evd projs =
   let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in
@@ -1407,7 +1407,7 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a
   if are_canonical_instances args1 args2 env then
     (* If instances are canonical, we solve the problem in linear time *)
     let sign = evar_filtered_context (Evd.find evd evk2) in
-    let id_inst = List.map_to_array (fun (id,_,_) -> mkVar id) sign in
+    let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in
     Evd.define evk2 (mkEvar(evk1,id_inst)) evd
   else
     let evd,ev1,ev2 =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 7d95e743d0..1394f3ba8c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -563,10 +563,12 @@ let meta_list evd = metamap_to_list evd.metas
 let find_meta evd mv = Metamap.find mv evd.metas
 
 let undefined_metas evd =
-  List.sort Pervasives.compare (map_succeed (function
-    | (n,Clval(_,_,typ)) -> failwith ""
-    | (n,Cltyp (_,typ))  -> n)
-    (meta_list evd))
+  let filter = function
+    | (n,Clval(_,_,typ)) -> None
+    | (n,Cltyp (_,typ))  -> Some n
+  in
+  let m = List.map_filter filter (meta_list evd) in
+  List.sort Pervasives.compare m
 
 let metas_of evd =
   List.map (function
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 96b57ae183..f32eb0879d 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -199,8 +199,8 @@ let canonical_projections () =
     !object_table []
 
 let keep_true_projections projs kinds =
-  map_succeed (function (p,(_,true)) -> p | _ -> failwith "")
-    (List.combine projs kinds)
+  let filter (p, (_, b)) = if b then Some p else None in
+  List.map_filter filter (List.combine projs kinds)
 
 let cs_pattern_of_constr t =
   match kind_of_term t with
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2a6dc35d14..3563e9ca26 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -188,7 +188,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   let reversible_rels = List.map fst li in
   if not (List.distinct reversible_rels) then
     raise Elimconst;
-  List.iter_i (fun i t_i ->
+  List.iteri (fun i t_i ->
     if not (List.mem_assoc (i+1) li) then
       let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
       if List.intersect fvs reversible_rels <> [] then raise Elimconst)