From dae4d95910bbdfabe8a8436ab954092ef4773e7d Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 24 Jun 2015 13:59:53 +0200
Subject: Add a comment about the use of a zipper, for clarity.

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

(limited to 'engine')

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
-- 
cgit v1.2.3