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

25 files changed, 150 insertions, 155 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index f43a03f4a5..a75aed5332 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -72,18 +72,20 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 let convert_string d =
   try id_of_string d
   with _ ->
-    if_verbose msg_warning
-      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
-    flush_all ();
-    failwith "caught"
+    if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+    raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = repr_dirpath coq_root in
-    let convert_dirs (lp,cp) =
-      (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
-    let dirs = map_succeed convert_dirs dirs in
+    let convert_dirs (lp, cp) =
+      try
+        let path = List.map convert_string (List.rev cp) @ prefix in
+        Some (lp, Names.make_dirpath path)
+      with Exit -> None
+    in
+    let dirs = List.map_filter convert_dirs dirs in
     List.iter Check.add_load_path dirs;
     Check.add_load_path (unix_path, coq_root)
   else
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 914a85fe8e..23fce79c1b 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -77,10 +77,14 @@ let revert_reserved_type t =
   try
     let l = Gmapl.find (constr_key t) !reserve_revtable in
     let t = Detyping.detype false [] [] t in
-    List.try_find
-      (fun (pat,id) ->
-	try let _ = Notation_ops.match_notation_constr false t ([], pat) in Name id
-	with Notation_ops.No_match -> failwith "") l
+    (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
+        then I've introduced a bug... *)
+    let find (pat, id) =
+      try let _ = Notation_ops.match_notation_constr false t ([], pat) in true
+      with Notation_ops.No_match -> false
+    in
+    let (_, id) = List.find find l in
+    Name id
   with Not_found | Failure _ -> Anonymous
 
 let _ = Namegen.set_reserved_typed_name revert_reserved_type
diff --git a/lib/cList.ml b/lib/cList.ml
index c5845e74ce..3e4c0a4b37 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -118,8 +118,7 @@ sig
   val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
-  val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
-  val try_find : ('a -> 'b) -> 'a list -> 'b
+  val find_map : ('a -> 'b option) -> 'a list -> 'b
   val uniquize : 'a list -> 'a list
 
   (** merges two sorted lists and preserves the uniqueness property: *)
@@ -143,7 +142,6 @@ sig
 
   (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
   val map_append : ('a -> 'b list) -> 'a list -> 'b list
-  val join_map : ('a -> 'b list) -> 'a list -> 'b list
 
   (** raises [Invalid_argument] if the two lists don't have the same length *)
   val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
@@ -169,14 +167,12 @@ sig
   val combinations : 'a list list -> 'a list list
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
 
-  (** Keep only those products that do not return None *)
-  val cartesian_filter :
-    ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+  (** Keep only those products that do not return None *)
 
-  val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val factorize_left : ('a * 'b) list -> ('a * 'b list) list
+
 end
 
 include List
@@ -555,12 +551,12 @@ let try_find_i f =
   in
   try_find_f
 
-let try_find f =
-  let rec try_find_f = function
-    | [] -> failwith "try_find"
-    | h::t -> try f h with Failure _ -> try_find_f t
-  in
-  try_find_f
+let rec find_map f = function
+| [] -> raise Not_found
+| x :: l ->
+  match f x with
+  | None -> find_map f l
+  | Some y -> y
 
 let uniquize l =
   let visited = Hashtbl.create 23 in
@@ -722,7 +718,6 @@ let drop_prefix p l =
       | None -> l
 
 let map_append f l = List.flatten (List.map f l)
-let join_map = map_append   (* Alias *)
 
 let map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
 
@@ -760,18 +755,6 @@ let rec assoc_f f a = function
   | (x, e) :: xs -> if f a x then e else assoc_f f a xs
   | [] -> raise Not_found
 
-(* Specification:
-   - =p= is set equality (double inclusion)
-   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
-   - let g = fun x -> f x [] in
-   - union_map f l acc =p= append (flatten (map g l)) acc
- *)
-let union_map f l acc =
-  List.fold_left
-    (fun x y -> f y x)
-    acc
-    l
-
 (* A generic cartesian product: for any operator (**),
    [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
    and so on if there are more elements in the lists. *)
@@ -817,4 +800,3 @@ let rec factorize_left = function
       (a,(b::List.map snd al)) :: factorize_left l'
   | [] ->
       []
-
diff --git a/lib/cList.mli b/lib/cList.mli
index 87eb3aee7d..ef4406150b 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -150,8 +150,10 @@ sig
   val assoc_snd_in_triple : 'a -> ('a * 'b * 'c) list -> 'b
   val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val sep_last : 'a list -> 'a * 'a list
-  val try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
-  val try_find : ('a -> 'b) -> 'a list -> 'b
+
+  val find_map : ('a -> 'b option) -> 'a list -> 'b
+  (** Returns the first element that is mapped to [Some _]. Raise [Not_found] if
+      there is none. *)
 
   val uniquize : 'a list -> 'a list
   (** Return the list of elements without duplicates. *)
@@ -184,9 +186,6 @@ sig
   val map_append : ('a -> 'b list) -> 'a list -> 'b list
   (** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)]. *)
 
-  val join_map : ('a -> 'b list) -> 'a list -> 'b list
-  (** Alias of [map_append]. *)
-
   val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
   (** As [map_append]. Raises [Invalid_argument _] if the two lists don't have 
       the same length. *)
@@ -215,14 +214,10 @@ sig
 
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
 
-  val cartesian_filter :
-    ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
-  (** Keep only those products that do not return None *)
-
   val cartesians_filter :
     ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
+  (** Keep only those products that do not return None *)
 
-  val union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val factorize_left : ('a * 'b) list -> ('a * 'b list) list
 end
 
diff --git a/lib/util.ml b/lib/util.ml
index 1025417310..6f9f9bd83f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -441,11 +441,6 @@ let interval n m =
   in
   interval_n ([],m)
 
-
-let map_succeed f l =
-  let filter x = try Some (f x) with Failure _ -> None in
-  List.map_filter filter l 
-
 (*s Memoization *)
 
 let memo1_eq eq f =
diff --git a/lib/util.mli b/lib/util.mli
index abfab29d56..a7586547ed 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -118,12 +118,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 
 val interval : int -> int -> int list
 
-
-(** In [map_succeed f l] an element [a] is removed if [f a] raises 
-   [Failure _] otherwise behaves as [List.map f l] *)
-
-val map_succeed : ('a -> 'b) -> 'a list -> 'b list
-
 (** {6 Memoization. } *)
 
 (** General comments on memoization:
diff --git a/library/nameops.ml b/library/nameops.ml
index 01a9a62403..5ea7e26855 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -114,7 +114,7 @@ let atompart_of_id id = fst (repr_ident id)
 
 let out_name = function
   | Name id -> id
-  | Anonymous -> failwith "out_name: expects a defined name"
+  | Anonymous -> failwith "Nameops.out_name"
 
 let name_fold f na a =
   match na with
diff --git a/library/nameops.mli b/library/nameops.mli
index c90aa7c782..fb26c1910d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -26,6 +26,8 @@ val lift_subscript   : identifier -> identifier
 val forget_subscript : identifier -> identifier
 
 val out_name : name -> identifier
+(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
+    otherwise. *)
 
 val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
 val name_iter : (identifier -> unit) -> name -> unit
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index b3fdd384a8..880d4b8ce1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -171,12 +171,13 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
   grammar_extend entry reinit (pos,[(name, p4assoc, [])])
 
 let pure_sublevels level symbs =
-  map_succeed
-    (function s ->
-       let i = level_of_snterml s in
-       if level = Some i then failwith "";
-       i)
-    symbs
+  let filter s =
+    try
+      let i = level_of_snterml s in
+      if level = Some i then None else Some i
+    with Failure _ -> None
+  in
+  List.map_filter filter symbs
 
 let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   List.fold_left (fun nb pt ->
@@ -260,11 +261,11 @@ let extend_grammar gram =
   grammar_state := (nb,gram) :: !grammar_state
 
 let recover_notation_grammar ntn prec =
-  let l = map_succeed (function
-    | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
-	 vars, x
-    | _ ->
-	 failwith "") !grammar_state in
+  let filter = function
+  | _, Notation (prec', vars, (_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+    Some (vars, x)
+  | _ -> None in
+  let l = List.map_filter filter !grammar_state in
   assert (List.length l = 1);
   List.hd l
 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 8fef987e6a..3a0840a7e1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -545,12 +545,15 @@ let rec list_mem_assoc_triple x = function
   | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l
 
 let register_empty_levels forpat levels =
-  map_succeed (fun n ->
-    let levels = (if forpat then snd else fst) (List.hd !level_stack) in
-    if not (list_mem_assoc_triple n levels) then
-      find_position_gen forpat true None (Some n)
-    else
-      failwith "") levels
+  let filter n =
+    try
+      let levels = (if forpat then snd else fst) (List.hd !level_stack) in
+      if not (list_mem_assoc_triple n levels) then
+        Some (find_position_gen forpat true None (Some n))
+      else None
+    with Failure _ -> None
+  in
+  List.map_filter filter levels
 
 let find_position forpat assoc level =
   find_position_gen forpat false assoc level
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)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 98cc42aaf5..b6b8f8dba3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1409,20 +1409,23 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
      - [subst0] is made of items [(p,u,(u,ty))] where [ty] is the type of [u]
        and both are adjusted to [extenv] while [p] is the index of [id] in
        [extenv] (after expansion of the aliases) *)
-  let subst0 = map_succeed (fun (x,u) ->
+  let map (x, u) =
     (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
     (* \--env-/          (= x:ty)         *)
     (* \--------------extenv------------/ *)
-    let (p,_,_) = lookup_rel_id x (rel_context extenv) in
+    let (p, _, _) = lookup_rel_id x (rel_context extenv) in
     let rec traverse_local_defs p =
       match pi2 (lookup_rel p extenv) with
       | Some c -> assert (isRel c); traverse_local_defs (p + destRel c)
       | None -> p in
     let p = traverse_local_defs p in
-    let u = lift (n'-n) u in
-    (p,u,expand_vars_in_term extenv u)) subst in
-  let t0 = lift (n'-n) t in
-  (subst0,t0)
+    let u = lift (n' - n) u in
+    try Some (p, u, expand_vars_in_term extenv u)
+      (* pedrot: does this really happen to raise [Failure _]? *)
+    with Failure _ -> None in
+  let subst0 = List.map_filter map subst in
+  let t0 = lift (n' - n) t in
+  (subst0, t0)
 
 let push_binder d (k,env,subst) =
   (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index da5ccc96b3..ce84e6bd5e 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -687,7 +687,8 @@ let simple_cases_matrix_of_branches ind brs =
       let nal,c = it_destRLambda_or_LetIn_names n b in
       let mkPatVar na = PatVar (Loc.ghost,na) in
       let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let ids = map_succeed Nameops.out_name nal in
+      let map name = try Some (Nameops.out_name name) with Failure _ -> None in
+      let ids = List.map_filter map nal in
       (Loc.ghost,ids,[p],c))
     brs
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9db16baac0..f8cd3609ad 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -217,12 +217,13 @@ let push_named_rec_types (lna,typarray,_) env =
     (fun e assum -> push_named assum e) env ctxt
 
 let lookup_rel_id id sign =
-  let rec lookrec = function
-    | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
-    | (n, (Name id',b,t)::l)  -> if id' = id then (n,b,t) else lookrec (n+1,l)
-    | (_, [])                 -> raise Not_found
+  let rec lookrec n = function
+    | []                     -> raise Not_found
+    | (Anonymous, _, _) :: l -> lookrec (n + 1) l
+    | (Name id', b, t) :: l  ->
+      if Names.id_ord id' id = 0 then (n, b, t) else lookrec (n + 1) l
   in
-  lookrec (1,sign)
+  lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
 let mkProd_or_LetIn (na,body,t) c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index b3e00ebaa1..b6bb438680 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -40,7 +40,10 @@ val print_env : env -> std_ppcmds
 val push_rel_assum : name * types -> env -> env
 val push_rels_assum : (name * types) list -> env -> env
 val push_named_rec_types : name array * types array * 'a -> env -> env
+
 val lookup_rel_id : identifier -> rel_context -> int * constr option * types
+(** Associates the contents of an identifier in a [rel_context]. Raise
+    [Not_found] if there is no such identifier. *)
 
 (** builds argument lists matching a block of binders or a context *)
 val rel_vect : int -> int -> constr array
diff --git a/tactics/auto.ml b/tactics/auto.ml
index be1e8e7017..d88a6a6b09 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -538,9 +538,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri ?(name=PathAny) (c,cty)
 
 let make_resolves env sigma flags pri ?name c =
   let cty = Retyping.get_type_of env sigma c in
-  let ents =
-    map_succeed
-      (fun f -> f (c,cty))
+  let try_apply f =
+    try Some (f (c, cty)) with Failure _ -> None in
+  let ents = List.map_filter try_apply
       [make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
   in
   if ents = [] then
@@ -912,11 +912,11 @@ let pr_hints_db (name,db,hintlist) =
 (* Print all hints associated to head c in any database *)
 let pr_hint_list_for_head c =
   let dbs = Hintdbmap.to_list !searchtable in
-  let valid_dbs =
-    map_succeed
-      (fun (name,db) -> (name,db, List.map (fun v -> 0, v) (Hint_db.map_all c db)))
-      dbs
+  let validate (name, db) =
+    let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in
+    (name, db, hints)
   in
+  let valid_dbs = List.map validate dbs in
   if valid_dbs = [] then
     (str "No hint declared for :" ++ pr_global c)
   else
@@ -941,7 +941,7 @@ let pr_hint_term cl =
 	with Bound -> Hint_db.map_none
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
-	map_succeed (fun (name, db) -> (name, db, fn db)) dbs
+      List.map (fun (name, db) -> (name, db, fn db)) dbs
     in
       if valid_dbs = [] then
 	(str "No hint applicable for current goal")
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1eecb1eb30..933bb6619a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -257,8 +257,8 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	       hints)
 	else []
       in
-        (hints @ map_succeed 
-	 (fun f -> try f (c,cty) with UserError _ -> failwith "") 
+        (hints @ List.map_filter
+	 (fun f -> try Some (f (c, cty)) with Failure _ | UserError _ -> None) 
 	 [make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri])
     else []
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7f2ee2e877..a35cf537e6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1075,20 +1075,21 @@ let simplify_args env sigma t =
 
 let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
-  let e_env = push_named (e,None,t) env in
-  let injectors =
-    map_succeed
-      (fun (cpath,t1',t2') ->
-        (* arbitrarily take t1' as the injector default value *)
-	let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
-	let injfun = mkNamedLambda e t injbody in
-	let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
-	let pf_typ = get_type_of env sigma pf in
-	let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
-        let pf = clenv_value_cast_meta inj_clause in
-	let ty = simplify_args env sigma (clenv_type inj_clause) in
-	(pf,ty))
-      posns in
+  let e_env = push_named (e, None,t) env in
+  let filter (cpath, t1', t2') =
+    try
+      (* arbitrarily take t1' as the injector default value *)
+      let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
+      let injfun = mkNamedLambda e t injbody in
+      let pf = applist(eq.congr,[t;resty;injfun;t1;t2]) in
+      let pf_typ = get_type_of env sigma pf in
+      let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
+      let pf = clenv_value_cast_meta inj_clause in
+      let ty = simplify_args env sigma (clenv_type inj_clause) in
+      Some (pf, ty)
+    with Failure _ -> None
+  in
+  let injectors = List.map_filter filter posns in
   if injectors = [] then
     errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
   tclTHEN
@@ -1493,7 +1494,8 @@ let subst_all ?(flags=default_subst_tactic_flags ()) gl =
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
     with PatternMatchingFailure -> failwith "caught"
   in
-  let ids = map_succeed test (pf_hyps_types gl) in
+  let test p = try Some (test p) with Failure _ -> None in
+  let ids = List.map_filter test (pf_hyps_types gl) in
   let ids = List.uniquize ids in
   subst_gen flags.rewrite_dependent_proof ids gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8e6fc8597e..69b446f90b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1024,9 +1024,11 @@ let progress_with_clause flags innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
   if ordered_metas = [] then error "Statement without assumptions.";
   let f mv =
-    find_matching_clause (clenv_fchain mv ~flags clause) innerclause in
-  try List.try_find f ordered_metas
-  with Failure _ -> error "Unable to unify."
+    try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause)
+    with Failure _ -> None
+  in
+  try List.find_map f ordered_metas
+  with Not_found -> error "Unable to unify."
 
 let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index af2ebc8d7a..ff6f004755 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -144,18 +144,20 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 let convert_string d =
   try Names.id_of_string d
   with _ ->
-    if_warn msg_warning
-      (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
-    flush_all ();
-    failwith "caught"
+    if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+    raise Exit
 
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
     let prefix = Names.repr_dirpath coq_root in
-    let convert_dirs (lp,cp) =
-      (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
-    let dirs = map_succeed convert_dirs dirs in
+    let convert_dirs (lp, cp) =
+      try
+        let path = List.map convert_string (List.rev cp) @ prefix in
+        Some (lp, Names.make_dirpath path)
+      with Exit -> None
+    in
+    let dirs = List.map_filter convert_dirs dirs in
     List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
     add_ml_dir unix_path;
     List.iter (Library.add_load_path false) dirs;