CODEWITHSUNDEEP
coq
user2423780
user2423780

Reputation: 73

How to get coq to print out new goal and hypotheses after applying tactic

sometimes I find coq gets into a state where when I apply a tactic, the new goal and hypotheses don't automatically get printed out. How do I set it to print these out after each tactic invocation.

This is coq 8.7.2, using coqtop

Upvotes: 1

Views: 340

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

I believe when this happens it's a bug in Proof General, which is supposed to display the proof context whenever you're in the middle of a proof. Li-yao Xia's solution of hitting C-c C-p should work.

Upvotes: 1

Related Questions