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

1 files changed, 3 insertions, 4 deletions

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|])::