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, 7 insertions, 6 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index aaf6f2bd09..9fe5606b97 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -152,7 +152,7 @@ let factor_fix env l cb msb =
     if List.length msb < n-1 then raise Impossible;
     let msb', msb'' = List.chop (n-1) msb in
     let labels = Array.make n l in
-    List.iter_i
+    List.iteri
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 01b98b1312..e3abab82b3 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -969,7 +969,7 @@ and simpl_case o typ br e =
 	    else ([], Pwild, ast_pop f)
 	  in
 	  let brl = Array.to_list br in
-	  let brl_opt = List.filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+	  let brl_opt = List.filteri (fun i _ -> not (Intset.mem i ints)) brl in
 	  let brl_opt = brl_opt @ [last_br] in
 	  MLcase (typ, e, Array.of_list brl_opt)
 	| None -> MLcase (typ, e, br)
@@ -1164,7 +1164,7 @@ let general_optimize_fix f ids n args m c =
     | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in List.iter_i aux args;
+  in List.iteri aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 6151abf6eb..4322ac95fa 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -877,7 +877,7 @@ let extract_inductive r s l optstr =
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
 	  optstr;
-	List.iter_i
+	List.iteri
 	  (fun j s ->
 	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 490d52555c..b820489f53 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1238,7 +1238,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
   let l = ref [] in
   let _ =
     try
-      List.iter_i
+      List.iteri
 	(fun i ((n,nt,is_defined) as param) ->
 	   if Array.for_all
 	     (fun l ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d8255e8342..bbc9ff93b3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -122,10 +122,11 @@ let generate_type g_to_f f graph i =
       | _ -> let j = !i in incr i;mkRel (nb_args - j  + 1)
   in
   (*i We need to name the vars [res] and [fv] i*)
+  let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
   let res_id =
     Namegen.next_ident_away_in_goal
       (id_of_string "res")
-      (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
+      (List.map_filter filter fun_ctxt)
   in
   let fv_id =
     Namegen.next_ident_away_in_goal