The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 08/12/2015 15:59, Robbert Krebbers wrote:
> On 12/08/2015 03:54 PM, Dominique Larchey-Wendling wrote:
>> 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 ?
> Maybe "Print Sorted Universes" will help. From the reference manual:
> 
>   If the optional Sorted option is given, each universe will
>   be made equivalent to a numbered label reflecting its level
>   (with a linear ordering) in the universe hierarchy.

Yes, that is the way to do it. For instance, Coq's testsuite executes
the following script:

Require all_stdlib.
Print Sorted Universes "universes.txt".

Then it parses the generated file to check that the number of universe
levels needed to typecheck the standard library did not unexpectedly change.

Best regards,

Guillaume