Apply the early check of the universe declaration and the monomorphic universe fixing to all interactive declarations

[herbelin]

Formerly, the early check (at Definition time) of the universe declaration and the monomorphic universe fixing (for asynchronous evaluation) were done only for Theorem and Definition without body (in post_check_evd). We do it also for interactive [Co]Fixpoint and for Program Fixpoint and Program Definition.

To anticipate what is done when proofs are completed, we apply UState.collapse_sort_variables and UState.restrict in some cases (this is needed for the test-suite to pass). But maybe should these be applied in all four cases, together with UState.normalize_variables and UState.minimize, as done at the end of proofs in general???

This gives an alternative solution to #15410 which allows to remove the forbidding for extensible universes introduced in #15424.

This remark at #15410 still hold though: "non extensible universe declarations don't make a lot of sense in universe monomorphic definitions", so maybe it can also be a failure.

• Added / updated test-suite.
• TODO: use the same check in all four situations (but which one?)

Depends on #18915 (merged)

[herbelin]

In two cases, comDefinition.ml and comProgramFixpoint.ml, I apparently need to do:

let check_univ_decl_early ~poly sigma udecl terms =
let vars = List.fold_left (fun acc b -> Univ.Level.Set.union acc (Vars.universes_of_constr b)) Univ.Level.Set.empty terms in
let uctx = Evd.evar_universe_context sigma in
let uctx = UState.collapse_sort_variables uctx in
let uctx = UState.restrict uctx vars in
UState.check_univ_decl ~poly uctx udecl

But in comFixpoint.ml and vernacentries.ml, collapse_sort_variable is not needed (for the examples of the test-suite to work). Is the need for collapse_sort_variable really expected or is it a revelator of a possible problem elsewhere?

[SkySkimmer]

The examples probably just don't generate free qvars.

[herbelin]

I'm asking because I found sometimes free qsort in the absence of minimization. Now, I also realize that vernacentries.ml and comFixpoint.ml do have a minimization and the others not. So, I have the feeling that what is finally needed is a minimization. I will try, thanks for the help.

[herbelin]

Finally, I used collapse_sort_variable since I saw it is already called by minimization and that, since the result is thrown away after checking, an (a priori) faster function is better.