coq - info_auto 策略在 Coq8.5 中不再打印痕迹？

Question

我曾经使用 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>

在消息 View 中。在其他场合，我有时会得到类似的东西

<unknown>; refine H

但这两者都没有帮助/信息，因为我无法应用这些来手动完成证明。

在 Coq 8.5 中复制旧的 info_auto 函数的正确方法是什么？

Answer 1

这个问题似乎已在 Coq 8.6 中得到修复。