aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2015-06-24 13:48:08 +0200
committerGravatar Cyprien Mangin <cyprien.mangin@m4x.org>2016-06-14 06:21:30 +0200
commit4962e042f3b2d7c5b089cec2dfe4e07a46bd2231 (patch)
tree37938138823eefd70e2f36d6e05405f8bd2de70f /engine
parent0f2b25d8b89a5ef3f3824b1840d97dd79a287d0e (diff)
Add a [CList.partitioni] function.
Diffstat (limited to 'engine')
-rw-r--r--engine/proofview.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index d1970abc9..2b8fc0057 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -409,10 +409,8 @@ let tclFOCUSLIST l t =
| [] -> tclZERO (NoSuchGoals 0)
| (mi, _) :: _ ->
let left, sub_right = CList.goto (mi-1) comb in
- let p x = CList.exists (fun (i, j) -> i <= x && x <= j) l in
- (* Since there is no [CList.partitioni], we do it manually. *)
- let sub = CList.filteri (fun x _ -> p (x + mi)) sub_right in
- let right = CList.filteri (fun x _ -> not (p (x + mi))) sub_right in
+ let p x _ = CList.exists (fun (i, j) -> i <= x +mi && x + mi <= j) l in
+ let sub, right = CList.partitioni p sub_right in
let mj = mi - 1 + CList.length sub in
Comb.set (CList.rev_append left (sub @ right)) >>
tclFOCUS mi mj t