coq - info_auto策略在Coq8.5中不再打印跟踪了吗？

我曾经使用info_auto来显示auto战术在幕后实际执行的步骤。但是，这似乎不再适用于Coq 8.5（beta3）。

以下示例用于Coq 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函数的正确方法是什么？

最佳答案

此问题似乎已在Coq 8.6中修复。