aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
authorherbelin2001-02-14 15:33:01 +0000
committerherbelin2001-02-14 15:33:01 +0000
commit4b77c47071645835f65740e6f4172f2c65ec6362 (patch)
treeeb4d9867ddfcf7bddc733ec6bd046243917435d9 /lib/util.ml
parente3fc07010b3fce8f9346b60cc12461f3ca123db6 (diff)
Restructuration
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1378 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml15
1 files changed, 7 insertions, 8 deletions
diff --git a/lib/util.ml b/lib/util.ml
index a518399937..9aee36e206 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -193,6 +193,13 @@ let list_try_find_i f =
in
try_find_f
+let list_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 list_uniquize = function
| [] -> []
| h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
@@ -259,14 +266,6 @@ let list_share_tails l1 l2 =
let list_join_map f l = List.flatten (List.map f l)
-let list_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
-
-
(* Arrays *)
let array_exists f v =