From 92616b9f660eaa2640964ca1925b05d37af70c8c Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 15 Sep 2012 00:39:54 +0000
Subject: 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
---
 lib/util.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'lib/util.ml')

diff --git a/lib/util.ml b/lib/util.ml
index 42ad11ee1f..1025417310 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -442,12 +442,9 @@ let interval n m =
   interval_n ([],m)
 
 
-let map_succeed f =
-  let rec map_f = function
-    | [] -> []
-    |  h::t -> try (let x = f h in x :: map_f t) with Failure _ -> map_f t
-  in
-  map_f
+let map_succeed f l =
+  let filter x = try Some (f x) with Failure _ -> None in
+  List.map_filter filter l 
 
 (*s Memoization *)
 
-- 
cgit v1.2.3