The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear Christian,

  There is documentation in dev/doc/universes about the changes necessary. The main idea is that if your tactic produces a term with polymorphic constants in it, it must produce one fresh instance of the constant at each use. Before giving the final proof term containing those fresh instances, you can call a type inference function to gather the universe constraints necessary for the whole term to typecheck automatically. Maybe a look at the OCaml code you use could help us fix this. 
The « cannot ensure that i <= j » error could also be because that constraint is not present in the graph you produce in a tactic I believe.

  The order-of-Imports issue is a bug for sure. Note that if you have a module A with everything polymorphic then importing it incurs no global constraints so the bug couldn’t happen in that case.

Best,
— Matthieu

Le lun. 10 sept. 2018 à 14:28, Christian Doczkal <christian.doczkal AT ens-lyon.fr> a écrit :

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