Discussion:
displaying goal and hypotheses
(too old to reply)
Jeremy Dawson
2018-11-14 23:19:21 UTC
Permalink
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
2018-11-15 10:35:48 UTC
Permalink
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
2018-11-15 12:09:44 UTC
Permalink
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
2018-11-15 13:11:58 UTC
Permalink
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
--
Enrico Tassi
Loading...