diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-06 09:37:03 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-06 09:37:03 +0000 |
| commit | a58fcc7439378bc2f4bdfb160e521f2dc11b9bb6 (patch) | |
| tree | 58d5096f1b31b6c270e4bfed0ff887f7251149fd /proofs/proof.mli | |
| parent | 89354342aa143eac0793cdef6abba7bcc5ce9806 (diff) | |
Fixed bullets so that they would play well with { }.
We can now have script like
assert P.
{ destruct n.
- solve_case1.
- solve_case2.
}
solve_goal
However there is an undesirable interaction with Focus (which we might, anyway, consider deprecated in favour of {}). Indeed, for compatibility with v8.3, Unfocus is called implicitely after each proof command if there is no focused goal. And the new behaviour of bullets is to allow arbitrary unfocusing command "pass trough" them. As a result, a script like
Focus.
split
- solves_first_goal
will result in a fully unfocused proof.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14262 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 23 |
1 files changed, 18 insertions, 5 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index cbde9244a..7de0a9fdf 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -85,11 +85,21 @@ val new_focus_kind : unit -> 'a focus_kind from it.*) type 'a focus_condition (* [no_cond] only checks that the unfocusing command uses the right - [focus_kind]. *) -val no_cond : 'a focus_kind -> 'a focus_condition + [focus_kind]. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{- solve_goal. }] because they use a loose-end condition. *) +val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* [done_cond] checks that the unfocusing command uses the right [focus_kind] - and that the focused proofview is complete. *) -val done_cond : 'a focus_kind -> 'a focus_condition + and that the focused proofview is complete. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{ - solve_goal. }] because they use a loose-end condition. *) +val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there @@ -97,8 +107,11 @@ val done_cond : 'a focus_kind -> 'a focus_condition val focus : 'a focus_condition -> 'a -> int -> proof -> unit exception FullyUnfocused +exception CannotUnfocusThisWay (* Unfocusing command. - Raises [FullyUnfocused] if the proof is not focused. *) + Raises [FullyUnfocused] if the proof is not focused. + Raises [CannotUnfocusThisWay] if the proof the unfocusing condition + is not met. *) val unfocus : 'a focus_kind -> proof -> unit (* [get_at_focus k] gets the information stored at the closest focus point |