Set Printing Universe 无效

Question

我正在关注 cpdt (http://adam.chlipala.net/cpdt/html/Universes.html) 中的 Universe 一章，该章节运行 Set Printing Universes. 以查看有关类型的其他评论。但是，我是运行 CoqIde 8.6，没有效果。

以下代码

Set Printing Universes.
Check Type.

产出

Type
    : Type

而书上说应该输出

Type (* Top.3 *)
     : Type (* (Top.3)+1 *)

我是不是漏掉了什么命令？我应该使用不同版本的 Coq 吗？

编辑：我刚刚在命令行中用 coqtop 尝试了这个，它确实打印了类型注释。也许我必须在 CoqIDE 中启用一些额外的选项？

Answer 1

是的，CoqIde 有专门的菜单："View" > "Display universe levels"。您可以从 "View" 菜单访问许多其他设置，但它们的对应命令（Unset Printing Notations. 等）对 CoqIde 无效。

Set Printing Universes has no effect