From 57d6f9018835ad73323fe0e33efec2bcc716db4c Mon Sep 17 00:00:00 2001 From: aspiwack Date: Wed, 4 Jul 2012 11:36:47 +0000 Subject: 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 --- proofs/proof.mli | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'proofs/proof.mli') 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 ***) -- cgit v1.2.3