diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 2b8fc00574..e497066b79 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -408,6 +408,8 @@ let tclFOCUSLIST l t = match l with | [] -> tclZERO (NoSuchGoals 0) | (mi, _) :: _ -> + (* [CList.goto] returns a zipper, so that + [(rev left) @ sub_right = comb]. *) let left, sub_right = CList.goto (mi-1) comb 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 |