Output of "Time" is hidden when this is the last goal in a "{...}"

[RalfJung]

Consider this Coq file:

Goal True /\ True.
Proof.
split.
{
Time tauto.

After stepping over the last command, I would expect to see the Coq output that tells me how long the command takes. Unfortunately, however, all PG shows in the *response* buffer is

This subproof is complete, but there are some unfocused goals.
         Try unfocusing with "}".

To figure out how long things take, I have to go back in the proof script and remove the {, and then remember to add it back before committing.

[RalfJung]

Actually the work-around does not even work in my situation as there is another tactic running first that requires there to be only one proof focused. So getting this time information will actually be some serious work. :/

[Matafou]

Thanks for reporting. I will have a look at it. Interestingly the timing is not put inside <infomsg>.

Another workaround is to switch off tidy response: (setq proof-tidy-response nil).