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

4 files changed, 32 insertions, 28 deletions

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