From 4962e042f3b2d7c5b089cec2dfe4e07a46bd2231 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 24 Jun 2015 13:48:08 +0200
Subject: Add a [CList.partitioni] function.

---
 engine/proofview.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index d1970abc9a..2b8fc00574 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
-- 
cgit v1.2.3