The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi,
>> - Require Import A B. succeeds
>> - Require Import B A. fails
>
> That sounds like a bug, you can open an issue on github with
> reproduction instructions and we will look into it.

Unfortunately, that's an internal repository with well over 10K lines,
and the problem occurs at the end. Should I manage to find a small
example, I will open an issue.

>> globalization of polymorphic reference <ID> would forget universes.
>
> Unfortunately various tactics and commands do not support or badly
> support universe polymorphism. This error means some function hasn't
> been adapted. It should probably be an anomaly.
> Depending on what exactly is failing it may be possible for us to fix
> it, or it could be beyond our current manpower.

This happens when calling one of our own tactics written in OCaml. So
how does one have to adapt tactics in order to properly support universe
polymorphism? (The error occurred while trying to see what happens if I
make just about everything universe polymorphic, so it may or may not be
necessary to fix this)

Thanks for the pointers,
Christian