aboutsummaryrefslogtreecommitdiff
path: root/tools.ml
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@chimrod.com>2017-11-01 20:06:02 +0100
committerSébastien Dailly <sebastien@chimrod.com>2017-11-01 20:06:02 +0100
commit041426ccc1b8c46578de38cd5a816a38158a51db (patch)
treed86ce5ab69ab291218ca07a637833fd0981d925c /tools.ml
parent9fbc5e48ea8183dda8fdb652364c0c29f8a309d5 (diff)
Moved range extraction function in ScTypes.ml
Diffstat (limited to 'tools.ml')
-rwxr-xr-xtools.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools.ml b/tools.ml
index 45c9bab..53b1c15 100755
--- a/tools.ml
+++ b/tools.ml
@@ -143,7 +143,7 @@ module List = struct
| [] -> raise Not_found
| hd::tl -> begin match f hd with
| Some x -> x
- | None -> find_map f tl
+ | None -> (find_map[@tailrec]) f tl
end
end