Search code examples
coqcoqide

Set Printing Universes has no effect

I'm following the Universes chapter in cpdt (http://adam.chlipala.net/cpdt/html/Universes.html), which runs Set Printing Universes. to see additional comments on the types. However, I'm running CoqIde 8.6 and it has no effect.

The following code

Set Printing Universes.
Check Type.

outputs

Type
    : Type

while the book says that it should output

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

Am I missing some command? Should I use a different version of Coq?

EDIT: I just tried this in the command line with coqtop and it does print the type annotations. Maybe I have to enable some additional option in CoqIDE?

Solution

  • Yes, CoqIde has a specific menu for this: "View" > "Display universe levels". There are quite a few other setting that you can access from the "View" menu, but their counterpart command (Unset Printing Notations., etc.) has no effect for CoqIde.