diff options
| author | aspiwack | 2012-02-07 16:51:59 +0000 |
|---|---|---|
| committer | aspiwack | 2012-02-07 16:51:59 +0000 |
| commit | beb59fba3298eddb1a47a96a51cb4cadc8aab821 (patch) | |
| tree | e6411912e0c2abf4136f1357d8d4d4c55997a4e1 | |
| parent | 1a305fc0410e70fc36f59623d1f0e618f7ee9aab (diff) | |
Additional comment on Focus Conditions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/proof.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 |