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 /man/coqchk.1 | |
| 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 'man/coqchk.1')
0 files changed, 0 insertions, 0 deletions