info_auto策略不會在Coq8.5中打印痕跡嗎？

Question

我曾經使用info_auto來顯示在引擎蓋下實際執行的步驟auto策略。但是，這似乎不再適用於Coq 8.5（beta3）。

下面的例子用來爲勒柯克8.4工作：

Example auto_example_5: 2 = 2. 
Proof. 
    info_auto. 
Qed. 

，並給我必要的步驟，例如apply @eq_refl.。

隨着Coq8.5，我得到一個警告：

The "info_auto" tactic does not print traces anymore. Use "Info 1 auto", instead. 
(* info auto : *) 

使用Info 1 auto.的暗示，我得到：

<unknown> 

在消息視圖。在其他場合，我有時會得到像

<unknown>; refine H 

但無論是很有幫助/信息，因爲我不能將這些手工完成的證明。

在Coq 8.5中複製舊info_auto函數的正確方法是什麼？

Answer 1

此問題似乎已在Coq 8.6中得到解決。