coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Find all universes in a term
Date: Fri, 21 Oct 2016 03:47:54 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f44.google.com
Ironport-phdr: 9a23:vlZ1MR1RYVL2IjfDsmDT+DRfVm0co7zxezQtwd8ZsegWL/ad9pjvdHbS+e9qxAeQG96KsbQZ2qGJ4+igATVGusnR9ihaMdRlbFwst4Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbsy8IIPZjty22uau4NWTJlwQ3HvuKY91eT6xtE36stQcyd9pLb90wR/UqFNJff5XzCVmPwTAsQz745Kf5pNs9D5B89co88NLUayyK6s9RLhVBzQvG28w7czv8xLESF3ctTMnTmwKn08QUED+5xbgU8K063Oiuw==

Hello --

Is there a way to get Coq to tell you where a universe comes from in a term? I know that you can do:

Set Printing All.

Set Printing Universes.

and then say:

Print foo.

To see all of the universe annotations, but this is giving me odd output for a particular function. In particular, the universe annotation is:

(* MirrorCore.EnvI.30 |= Set <= MirrorCore.EnvI.30

MirrorCore.EnvI.30 <= Coq.Init.Datatypes.51

Urefl <= MirrorCore.EnvI.30

But when I search the text of the term, MirrorCore.EnvI.30 does not occur anywhere.

Any pointers would be greatly appreciated.

[Coq-Club] Find all universes in a term, Gregory Malecha, 10/21/2016
- Re: [Coq-Club] Find all universes in a term, Jason Gross, 10/21/2016
  - Re: [Coq-Club] Find all universes in a term, Matthieu Sozeau, 10/21/2016
    - Re: [Coq-Club] Find all universes in a term, Gregory Malecha, 10/21/2016