From 17ca9766c45ebb368558712eff18d0ed71583e66 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Tue, 20 Mar 2012 17:46:48 +0000 Subject: 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 --- proofs/proof.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'proofs/proof.mli') 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 -- cgit v1.2.3