Как заставить coq распечатать новую цель и гипотезу после применения тактики

Question

иногда я нахожу, что coq попадает в состояние, когда при применении тактики новая цель и гипотезы не распечатываются автоматически.Как мне настроить его вывод на печать после каждого вызова тактики.

Это coq 8.7.2 с использованием coqtop

Answer 1

Я полагаю, что когда это происходит, это ошибка в Proof General, которая должна отображать контекст доказательства, когда вы находитесь в середине доказательства. Решение Ли-Яо Ся удара C-c C-p должно работать.