The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hello Talia,

Talia Ringer 
<tringer AT cs.washington.edu>
 writes:

> 1. A way to tell type-checking from within a plugin about the universe
> constraints so that it knows to solve them correctly, or
>
> 2. a way to tell type-checking from within a plugin to just assume all
> universe constraints go through, because this will always be true for me,
> and if it isn't, then the plugin will just fail later anyways
>
> I'm assuming #1 is the proper way to call type-checking from within a
> plugin, but I'm not sure how to do it.

So indeed as others have pointed out, the kernel won't infer constraints
for you anymore so you'll have to manually infer them [very cumbersome]
or call the type inference mechanism.

Coq devs are aware the universe-handling API could certainly take some
usability improvements, please, as an API user don't hesitate to share
thoughts or suggestions about it.

I think that the preferred interface these is to open an issue on
GitHub, but of course mailing list discussion is welcome too [however it
has the downside that, contrary to GH issues, it tends to be harder to
translate to concrete actionable plans].

Best,
E.