From beb59fba3298eddb1a47a96a51cb4cadc8aab821 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 7 Feb 2012 16:51:59 +0000
Subject: Additional comment on Focus Conditions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 83ed0ffe14..2f2c3a1696 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -72,7 +72,10 @@ module Cond = struct
      - [Loose] that the condition is not quite met
        but authorises to unfocus provided a condition
        of a previous focus on the stack is (strictly)
-       met.
+       met. [Loose] focuses are those, like bullets,
+       which do not have a closing command and
+       are hence closed by unfocusing actions unrelated
+       to their focus_kind.
   *)
   let bool b =
     if b then fun _ _ -> Strict
@@ -359,6 +362,7 @@ let no_focused_goal p =
 
 (*** Proof Creation/Termination ***)
 
+(* [end_of_stack] is unfocused by return to close every loose focus. *)
 let end_of_stack_kind = new_focus_kind ()
 let end_of_stack = done_cond end_of_stack_kind
 
-- 
cgit v1.2.3