I think I started learning Coq around March 2012, so it must have been
8.3pl3 or 8.3pl4.
Setting coq-end-goals-regexp-show-subgoals to nil does what I want (or, at
least, is plenty good). Thanks for the workaround!
-Jason
On Fri, Apr 19, 2013 at 4:55 AM, Hendrik Tews wrote:
>
> I believe all
I believe all Proof General versions (including the latest trunk)
show the timing in the *goals* buffer when you use them with Coq
8.3pl4 or earlier. If you have more than one subgoal the timing
is shown only when coq-hide-additional-subgoals is off. Then the
*goals* buffer looks like
###
I remember how PG used to behave, but I do not recall which version it was.
I started using Coq at version 8.3pl2, or there-abouts, so I can try to
8.3pl3 was released in December 2011, so it was probably Proof
General 4-2pre111207 or earlier.
Hendrik
__
I remember how PG used to behave, but I do not recall which version it was.
I started using Coq at version 8.3pl2, or there-abouts, so I can try to
figure out which version of PG behaved how I expect. I will try to get
back to the email list within the next few days with a response about this.
-
