More cleaning on Utils and CList. Some parts of the code being

peculiarly messy, I hope I did not introduce too many bugs.

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

6 files changed, 34 insertions, 31 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 9fe5606b97..2baea11a33 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,17 +30,24 @@ let toplevel_env () =
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
 	let mp,_,l = repr_kn kn in
-	let seb = match Libobject.object_tag o with
-	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
-	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
-	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+	begin match Libobject.object_tag o with
+	  | "CONSTANT" ->
+            let constant = Global.lookup_constant (constant_of_kn kn) in
+            Some (l, SFBconst constant)
+	  | "INDUCTIVE" ->
+            let inductive = Global.lookup_mind (mind_of_kn kn) in
+            Some (l, SFBmind inductive)
+	  | "MODULE" ->
+            let modl = Global.lookup_module (MPdot (mp, l)) in
+            Some (l, SFBmodule modl)
 	  | "MODULE TYPE" ->
-	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
-	  | _ -> failwith "caught"
-	in l,seb
-    | _ -> failwith "caught"
+            let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+            Some (l, SFBmodtype modtype)
+	  | _ -> None
+        end
+    | _ -> None
   in
-  SEBstruct (List.rev (map_succeed get_reference seg))
+  SEBstruct (List.rev (List.map_filter get_reference seg))
 
 
 let environment_until dir_opt =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 78126bc16a..826dcec02d 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,7 @@ and pp_module_type params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (mp, sign) ->
       push_visible mp params;
-      let l = map_succeed pp_specif sign in
+      let l = List.map pp_specif sign in
       pop_visible ();
       str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +707,7 @@ and pp_module_expr params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEstruct (mp, sel) ->
       push_visible mp params;
-      let l = map_succeed pp_structure_elem sel in
+      let l = List.map pp_structure_elem sel in
       pop_visible ();
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 18b2bbe2f7..edc727a48f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -97,11 +97,7 @@ let functional_induction with_clean c princl pat =
       if with_clean
       then
 	let idl =
-	  map_succeed
-	    (fun id ->
-	       if Idset.mem id old_idl then failwith "subst_and_reduce";
-	       id
-	    )
+	  List.filter (fun id -> not (Idset.mem id old_idl))
 	    (Tacmach.pf_ids_of_hyps g)
 	in
 	let flag =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bbc9ff93b3..7be8328a74 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -116,10 +116,13 @@ let generate_type g_to_f f graph i =
       | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type
   in
   let nb_args = List.length fun_ctxt in
-  let args_from_decl i decl =
-    match decl with
-      | (_,Some _,_) -> incr i; failwith "args_from_decl"
-      | _ -> let j = !i in incr i;mkRel (nb_args - j  + 1)
+  let rec args_from_decl i accu = function
+  | [] -> accu
+  | (_, Some _, _) :: l ->
+    args_from_decl (succ i) accu l
+  | _ :: l ->
+    let t = mkRel (nb_args - i + 1) in
+    args_from_decl (succ i) (t :: accu) l
   in
   (*i We need to name the vars [res] and [fv] i*)
   let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
@@ -131,12 +134,11 @@ let generate_type g_to_f f graph i =
   let fv_id =
     Namegen.next_ident_away_in_goal
       (id_of_string "fv")
-      (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
+      (res_id::(List.map_filter (function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None) fun_ctxt))
   in
   (*i we can then type the argument to be applied to the function [f] i*)
   let args_as_rels =
-    let i = ref 0 in
-    Array.of_list ((map_succeed (args_from_decl i) (List.rev fun_ctxt)))
+    Array.of_list (args_from_decl 0 [] fun_ctxt)
   in
   let args_as_rels = Array.map Termops.pop args_as_rels in
   (*i
@@ -152,8 +154,7 @@ let generate_type g_to_f f graph i =
     i*)
   let graph_applied =
     let args_and_res_as_rels =
-      let i = ref 0 in
-      Array.of_list ((map_succeed (args_from_decl i) (List.rev ((Name res_id,None,res_type)::fun_ctxt))) )
+      Array.of_list (args_from_decl 0 [] ((Name res_id,None,res_type) :: fun_ctxt))
     in
     let args_and_res_as_rels =
       Array.mapi (fun i c -> if i <> Array.length args_and_res_as_rels - 1 then lift 1 c else c) args_and_res_as_rels
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8b0fc27397..ec1994cd0c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -667,11 +667,10 @@ let mkDestructEq :
   fun not_on_hyp expr g ->
   let hyps = pf_hyps g in
   let to_revert =
-    Util.map_succeed
-      (fun (id,_,t) ->
+    Util.List.map_filter
+      (fun (id, _, t) ->
         if List.mem id not_on_hyp || not (Termops.occur_term expr t)
-        then failwith "is_expr_context";
-        id) hyps in
+        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
   let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 6c6e2c57f2..c6256b0c50 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -929,10 +929,10 @@ let filter_compatible_systems required systems =
   let rec select = function
       (x::l) ->
 	if List.mem x required then select l
-	else if List.mem (barre x) required then failwith "Exit"
+	else if List.mem (barre x) required then raise Exit
 	else x :: select l
     | [] -> [] in
-  map_succeed (function (sol,splits) -> (sol,select splits)) systems
+  List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems
 
 let rec equas_of_solution_tree = function
     Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)