The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

In this particular case you should look what Coq.Init.Datatypes.51 corresponds to, probably some inductive parameter, and see to what the inductive is applied in your term. 

On Fri, Oct 21, 2016 at 6:02 AM Jason Gross <jasongross9 AT gmail.com> wrote:

Note that reduction can leave over floating universes
Definition foo := Eval hnf in let T := Type in let enforce := (Type : (Type : T)) in T.
Perhaps it comes from that, or from tactics?

On Thu, Oct 20, 2016, 11:48 PM Gregory Malecha <gmalecha AT gmail.com> wrote:

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.

--

- gregory malecha
  gmalecha.github.io