3

我过去常常用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

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

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

4

1 回答 1

2

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

于 2017-08-19T05:01:28.067 回答