如何讓COQ編寫完整的校對日誌？

Question

我希望COQ在執行證明時記錄其所有子目標。 COQC的-verbose選項沒有給出正確的結果。

二，有沒有讓COQ記錄汽車，直覺等戰術所用的所有基本策略的選項？

Answer 1

在勒柯克的最新版本（> = 8.7，我認爲），你可以發出

Set Ltac Debug. 
Set Ltac Batch Debug. 

，並獲得戰術執行的非常詳細的日誌，正在面臨的各種目標。