如何让coq在应用策略后打印出新的目标和假设

Question

有时我发现coq进入了一种状态，当我应用策略时，新的目标和假设不会自动打印出来。我如何设置它在每次策略调用后打印这些内容。

这是coq 8.7.2，使用coqtop

Answer 1

我相信当这种情况发生时，这是Proof General中的一个bug，它应该在您进行证明时显示证明上下文。李耀霞对C-c C-p的解决方案应该是有效的。