[Coq-Club] displaying goal and hypotheses

[Jeremy Dawson]

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)

[Pierre Courtieu]

Hi, It looks like a problem with the interface. Which one do you use?
coqide, Proofgeneral, something else?
Pierre

Post by Jeremy Dawson
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
Thanks
Jeremy

[Jeremy Dawson]

Hi,

I just type coqtop (actually coqtop -color no) into a terminal window.

Sorry if I don't understand your question.

Cheers,

Jeremy

Post by Pierre Courtieu
Hi, It looks like a problem with the interface. Which one do you use?
coqide, Proofgeneral, something else?
Pierre
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
Thanks
Jer

[Enrico Tassi]

Post by Jeremy Dawson
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