✨ Add coq.univ.super

[ecranceMERCE]

Short utility function to make Type@{i+1}

[gares]

Please rebase on master the diff is spurious otherwise.

I sort of recall @ppedrot saying that "sorts have a super, not universes", but maybe I'm wrong and this API is OK. Maybe it was about max?

[ecranceMERCE]

sorts have a super, not universes

There is Univ.Universe.super and Sorts.super, I do not really know the difference.

[ecranceMERCE]

I would have liked to add the following test to test_API_typecheck.v:

Elpi Query lp:{{
  coq.typecheck (sort (typ U)) T ok,
  coq.unify-eq T (sort (typ {coq.univ.super U})) ok.
}}.

i.e. making sure that in Type@{i} : T, T can be forced to be Type@{i+1}.

However I get the following error and cannot understand its source:

Unable to unify "Type@{test_API_typecheck.34}" with
 "Type@{test_API_typecheck.33+1}"
(universe inconsistency: Cannot enforce test_API_typecheck.34 =
test_API_typecheck.33+1).

I can just say that in my local version of Coq-Elpi (mainly disabling purge_algebraic_univs_sort), this utility function seems to work and helps in filling all type annotations before declaring universe polymorphic inductives with coq.env.add-indt.

[gares]

I saw a message by @CohenCyril on this very topic on zulip, and the answer was that Coq's universe constraint system is not able to represent this constraints (at least not always)...

[CohenCyril]

I saw a message by @CohenCyril on this very topic on zulip, and the answer was that Coq's universe constraint system is not able to represent this constraints (at least not always)...

This is a different problem, I think

[CohenCyril]

Indeed the use case here is actually for #401 which is accepted by Coq but undoable in elpi as of today