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

2 files changed, 5 insertions, 6 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4d67fef00..7f2ee2e87 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1410,17 +1410,16 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
   (* The set of hypotheses using x *)
   let depdecls =
     let test (id,_,c as dcl) =
-      if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl
-      else failwith "caught" in
-    List.rev (map_succeed test (pf_hyps gl)) in
+      if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then Some dcl
+      else None in
+    List.rev (List.map_filter test (pf_hyps gl)) in
   let dephyps = List.map (fun (id,_,_) -> id) depdecls in
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var (pf_env gl) x (pf_concl gl) in
   (* The set of non-defined hypothesis: they must be abstracted,
      rewritten and reintroduced *)
   let abshyps =
-    map_succeed
-      (fun (id,v,_) -> if v=None then mkVar id else failwith "caught")
+    List.map_filter (function (id, None, _) -> Some (mkVar id) | _ -> None)
       depdecls in
   (* a tactic that either introduce an abstracted and rewritten hyp,
      or introduce a definition where x was replaced *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4ce382df2..057a268f5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1242,7 +1242,7 @@ let rec extract_ids ids = function
 let default_fresh_id = id_of_string "H"
 
 let interp_fresh_id ist env l =
-  let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
+  let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
   let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in
   let id =
     if l = [] then default_fresh_id