diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-04 11:36:47 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-04 11:36:47 +0000 |
| commit | 57d6f9018835ad73323fe0e33efec2bcc716db4c (patch) | |
| tree | 7c10ab40dc5ef3d16dea61ab5ee0631d16d55559 /proofs/proof.mli | |
| parent | d153f3da0dc05d829fb3e0c234b555e170d0c074 (diff) | |
Change how the number of open goals is printed.
If you are focused on 3 subgoals, and unfocusing would reveal 2 extra
subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop
will tell you:
3 focused subgoals (unfocused: 2-4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index e162a2aa0..d0b7e9839 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -34,6 +34,15 @@ open Term (* Type of a proof. *) type proof +(* Returns a stylised view of a proof for use by, for instance, + ide-s. *) +(* spiwack: the type of [proof] will change as we push more refined + functions to ide-s. This would be better than spawning a new nearly + identical function everytime. Hence the generic name. *) +(* In this version: returns the focused goals, a representation of the + focus stack (the number of goals at each level) and the underlying + evar_map *) +val proof : proof -> Goal.goal list * int list * Evd.evar_map (*** General proof functions ***) |