diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2015-06-24 13:48:08 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:30 +0200 |
| commit | 4962e042f3b2d7c5b089cec2dfe4e07a46bd2231 (patch) | |
| tree | 37938138823eefd70e2f36d6e05405f8bd2de70f /engine/proofview.ml | |
| parent | 0f2b25d8b89a5ef3f3824b1840d97dd79a287d0e (diff) | |
Add a [CList.partitioni] function.
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 6 |
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 |