diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2015-06-24 13:59:53 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:30 +0200 |
| commit | dae4d95910bbdfabe8a8436ab954092ef4773e7d (patch) | |
| tree | 45f7d3a3450b3e632ed0daeb33ff36291fdac0bc /engine/proofview.ml | |
| parent | 8beceb7e73480c72b8e9d319d94ae1a9202418a5 (diff) | |
Add a comment about the use of a zipper, for clarity.
Diffstat (limited to 'engine/proofview.ml')
| -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 2b8fc0057..e497066b7 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 |