Fix two BadVarianceQ anomalies in inductive cumulativity

[JasonGross]

Two independent BadVarianceQ anomalies, one per commit. Both are cases where the
universe path is handled and the sort-quality path was never wired up alongside it.

1. Valid declaration anomalies when the quality check needs delta unfolding

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Definition idT@{s;u} (A:Type@{s;u}) : Type@{s;u} := A.
Inductive t@{*s;u} (A:Type@{s;u}) : Prop := c (_ : idT A).

Anomaly "Uncaught exception InferCumulativity.BadVarianceQ(_, 0, 2)."

Expected: accepted, since unfolding idT satisfies the annotation. The universe
analogue Inductive t@{s;*u} (A:Type@{s;u}) : Prop := c (_ : idT A). is accepted.

The FFlex (ConstKey _) case of infer_cumul_stack (kernel/inferCumulativity.ml:284)
retries after unfolding when the constant's recorded variance fails the check, but its
handler listed only BadVariance, so the quality counterpart escaped. In Infer mode the
same position raises NotInferring, which was caught — hence the anomaly is Check-mode
only.

Check mode is entered two ways: an explicit variance annotation as above, or rocqchk,
which maps every recorded variance to Some v (checker/checkInductive.ml:99) and so
runs every cumulative inductive in Check mode with no user syntax. That is the route in
theorem-labs/grading-tools#287, where the anomaly follows the line
checking cst:IsomorphismChecker.IsomorphismDefinitions.from_to. That label is
misleading: mod_checking prints no progress line for inductives
(checker/mod_checking.ml:290), only for constants, modules and module types, so the
constant named is the previous declaration, not the failing one.

2. Invalid annotation anomalies instead of erroring

Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Inductive t@{*s;u} : Prop := c (_ : Type@{s;u}).

Anomaly "Uncaught exception InferCumulativity.BadVarianceQ(_, 0, 1)."

Expected: a type error. infer_inductive converted BadVariance to a type error but
left BadVarianceQ; the universe analogue t@{s;*u} already reports
Incorrect variance for universe. No constant is involved here, so commit 1 does not
cover this case.

Adds BadQVariance to ptype_error and prints it the same way as BadVariance:

Error: Incorrect variance for sort quality α1: expected * but cannot be less restrictive than +.

The qvar prints as α1 rather than s because Termops.pr_evd_qvar is used, matching
explain_undeclared_qualities; the universe analogue likewise prints d2u.1 rather than
u. Not changed here.

checker/coqchk_main.ml gains a one-line arm for the new constructor; without it the
checker does not compile.

Tests

test-suite/success/CumulInd.v gains quality analogues of the file's existing
not_irrelevant, check_covariant and must_unfold universe cases. The whole file runs
at rc=0 with no Error/Anomaly output after the patch.

Measured at

Base c9469b7be409866c36dc12556350d3cd940fe80a (v9.2+typewise-isomorphism), 9.2+rc2,
OCaml 4.14.2. dune build -p rocq-runtime, dune build topbin/rocqworker.exe and
dune build rocq-core.install all rc=0.

Not applicable upstream: sort quality variance does not exist in rocq-prover/rocq master
(6df5ae331262750d9fc2d115dd2198a6373e4dd0), whose inferCumulativity.ml carries
(* no variance for qualities *) and whose infer_inductive takes no quals argument.
The feature entered this fork with 77b78068d4a34787f50d0550870189ce0206d1ec, cherry-picked
from rocq-prover#21773, which was closed unmerged.

Other affected branches

BadVarianceQ is present in kernel/inferCumulativity.ml on 6 of 16 branches of this
repo, and the six touched files are blob-identical across all six, so both commits apply
unchanged: v9.2+typewise-isomorphism, v9.2+typewise-isomorphism-stable,
v9.2+typewise-isomorphism+rocq-dune, backport/22294-v9.2-typewise-isomorphism,
backport/22294-v9.2-typewise-isomorphism-stable, codex/restricted-model-thin-slice.

🤖 Generated with Claude Code