The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear all,

May be it is a simple question, but is it possible to bound the Type
hierarchy to some finite number while compiling a proof. The goal
could be for instance to determine the least size of the hierarchy
for a proof to type-check ?

Another way to formulate the question is how can I know the maximum
n such that Type_n is needed in the type-checking of a given proof ?

Of course, this might imply that all the parameters have a fixed
Type index which could be obtained by replacing

forall (X : Type) ...

by

forall (X : Set) ...

for instance.

It seems to me that Set Printing Universes is not enough for that.

Dominique