The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Thu, 9 Feb 2012 14:12:44 -0500,
Gregory Malecha 
<gmalecha AT eecs.harvard.edu>
 a écrit :

> Hello,
> 
> Is there any way in Coq to search for the term (or terms) that
> generated a universe constraint? Normally, I can get some idea from
> the name of the variables involved, but I currently have a universe
> variable that I can't find occuring anywhere.
> 
> Thank you.
> 

None that I know of.
You can manually name some universes, for instance:

Definition T0 := Type.
Definition T1 := Type.

Inductive poly_list : T0 :=
| Nil : poly_list
| Cons : forall (A:T1), A -> poly_list -> poly_list
.

or even set universe constraints manually:

Definition T0 := Type.
Definition T1 := Type:T0.
(*                   ^^^*)

Inductive poly_list : T0 :=
| Nil : poly_list
| Cons : forall (A:T1), A -> poly_list -> poly_list
.

Defining and using a new Type each time you need it; but universe
variables are awfull to track in Coq (each time you replay a
definition/proof, new identifiers will be generated). I think it would
be a lot better if all these stuff were pervasives (ie. replaying the
same code in the same universe context, will generate the same
identifiers for universe variable).

So you can use the trick of naming types universes, it is not very
exiting, but you can gain a slight speed up during universe resolution
(if you resolve by hand your universes, you ease this computation), and
probably can more easily find generated some universe constraint.