diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 17:46:48 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-20 17:46:48 +0000 |
| commit | 17ca9766c45ebb368558712eff18d0ed71583e66 (patch) | |
| tree | 4884bb30e5acaecccc941a214c4de9484718ae37 /proofs/proof.mli | |
| parent | 52b57c6c529d1896ee73890db9faf3d299619403 (diff) | |
Arranged for the desirable behaviour that bullets do not see beyond braces.
i.e.: after a brace is open, one can use the bullets again without clashing with
bullets outside the brace. In particular, one can nest bullets with arbitrary
depth (by interleaving them with occasional braces).
Also fixed a typo introduced in my previous commit which caused bullets
and braces to behave just like regular focuses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15073 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index ae3430535..ef402fe60 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -120,6 +120,9 @@ val unfocus : 'a focus_kind -> proof -> unit exception NoSuchFocus val get_at_focus : 'a focus_kind -> proof -> 'a +(* [is_last_focus k] check if the most recent focus is of kind [k] *) +val is_last_focus : 'a focus_kind -> proof -> bool + (* returns [true] if there is no goal under focus. *) val no_focused_goal : proof -> bool |