The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This might be an issue with a recent change to template polymorphism.  As I note in https://github.com/coq-community/coq-ext-lib/pull/76, many inductives in coq-ext-lib that were template polymorphic in Coq 8.9 are no longer polymorphic in Coq 8.10.  If you are using Coq 8.10, you can test if this is your issue by recompiling and reinstalling coq-ext-lib from source after adding `Unset Template Check` to the top of the OptionMonad file.  (Note that this flag is unsafe and permits proofs of False.  The correct fix is to either (a) move the inductive out of the section, (b) enable full universe polymorphism, or (c) wait for the Coq devs to finish implementing proper sort-polymorphism which should allow backwards-compatible template-polymorphism on top of it.)

On Mon, Dec 2, 2019, 11:49 Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

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
>