The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, 2018-11-14 at 23:19 +0000, Jeremy Dawson wrote:
> Hi coq-club,
> 
> thanks for all the answers to my previous question
> 
> sometimes I find coq gets into a state where when I apply a tactic,
> the 
> new goal and hypotheses don't automatically get displayed. How do I 
> reset it to show these after each tactic invocation?
> 
> (typing Show. works fine, but it's a nuisance to do it for each
> tactic)
> 
> This is coq 8.7.2, using coqtop

I think you should try to see if the bug is still there in Coq 8.8.2
and eventually report the issue at
  https://github.com/coq/coq/issues

As a side note, the bare bone coqtop is mainly a development/debugging
tool. I would not recommend it as an "interface" for developing proofs.

Best
-- 
Enrico Tassi