diff options
| author | aspiwack | 2012-03-30 12:51:23 +0000 |
|---|---|---|
| committer | aspiwack | 2012-03-30 12:51:23 +0000 |
| commit | c2c41a164c5eecc62995752ec9e22904cf7e7cd1 (patch) | |
| tree | 7c9f9a707f0906ce0fb21b16188e29bd425a851e /proofs/proof.mli | |
| parent | 1e1b6828c29b1344f50f94f9d3a6fce27a885656 (diff) | |
Added a command "Unfocused" which returns an error when the proof is
not fully unfocused (in the style of the Guarded command).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 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 ef402fe606..715b3341b6 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -114,6 +114,9 @@ exception CannotUnfocusThisWay is not met. *) val unfocus : 'a focus_kind -> proof -> unit +(* [unfocused p] returns [true] when [p] is fully unfocused. *) +val unfocused : proof -> bool + (* [get_at_focus k] gets the information stored at the closest focus point of kind [k]. Raises [NoSuchFocus] if there is no focus point of kind [k]. *) |