The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

With Coq >=8.10 the universes may have nicer names like 
Coq.Lib.File.def.u0 which can be used in commands.

Gaëtan Gilbert

On 02/12/2019 17:15, Christian Doczkal wrote:
> Hi
>
> On 01/12/2019 18:20, Vadim Zaliva wrote:
> > “If it is indeed failing to enforce [Helix.MSigmaHCOL.Memory.16 < 
> > Coq.FSets.FMapAVL.649], then you may get away with enforcing early that the 
> > universe for FMap contents is strictly larger than the universe for Memory 
> > contents.”
> >
> > How can I enforce something like this?
> If you use explicit universes in the definitions for instance as follows:
>
> Universe U.
> Definition foo (T : Type@{U}) ...
>
> Then you can pose constraints:
>
> Constraint U < V.
>
> See also: 
> https://coq.inria.fr/distrib/current/refman//addendum/universe-polymorphism.html?highlight=constraint#explicit-universes
>
> In my case, where all definitions involved in the conflict where within the 
> library I was working in, this was sufficient.
>
> I'm not sure what's the best way to give a name to a universe that's 
> introduced in a library one is importing (e.g., introduce a universe U and 
> then define an object that generates the constraint U = Coq.Lib.File.n *). 
> Maybe someone else can comment on that.
>
> Best,
> Christian