safechecker-plugin: adapt for a 9.2 base carrying the backported 9.3 assumptions API (rocq#22164)

[claude-fable-5-theorem]

Bottom line

We build a Rocq fork that is 9.2 plus one backported 9.3 API. That backport — not anything in
MetaRocq — is why this 9.2-targeting branch no longer compiles for us. The one-line change here
fixes our build, and it would break cumul-sort-poly-fix for anyone on a released 9.2.

So this is a question, not really a merge request. What we'd like from you, in preference order:

1. A variant branch (e.g. cumul-sort-poly-fix+22164) carrying this commit, which costs your
   other users nothing. This is the ask.
2. Tell us to carry it locally — completely fine, and it's what we're doing today. If you do
   nothing, this is the outcome and nothing of ours is blocked.
3. Merge it here — only if you're happy for cumul-sort-poly-fix to stop supporting stock 9.2.
   We are not asking for this.

Close this PR freely if (2) is your answer. We opened it mainly so the divergence is visible to you
rather than silently vendored in our image build.

Why a 9.2 branch is hitting a 9.3 signature

rocq-prover/rocq#22164 changed
Assumptions.assumptions to return a pair. It is milestoned 9.3+rc1 and landed on Rocq
master, so stock 9.2 is unaffected and cumul-sort-poly-fix is correct as it stands.

Our fork (theorem-labs/rocq, v9.2+typewise-isomorphism) cherry-picked that change onto a 9.2
base in June, before it merged upstream. The result is a toolchain that reports itself as 9.2 but
exposes one 9.3 signature — a configuration that exists nowhere upstream. We made this problem;
we're not claiming MetaRocq broke anything.

You already made exactly this adaptation upstream in MetaRocq#1287 ("Adapt to rocq-prover/rocq#22164") on
main. This PR just carries that same one-liner to the 9.2-targeting branch, which is why the diff
should look familiar.

No conditional can paper over it: our fork self-reports as 9.2, so version macros can't separate the
two cases, and OCaml won't accept both shapes from one expression.

Build error, and why we can't just move our pin

File "src/g_metarocq_safechecker.mlg", line 93, characters 50-54:
Error: This expression has type
         Printer.theory_assumptions * Constr.types Printer.ContextObjectMap.t
       but an expression was expected of type 'a Printer.ContextObjectMap.t

RocqCheck's retypecheck_term_dependencies only consumes the dependency map (it retypechecks each
dependency), so discarding the theory flags is the sound choice for a retypechecking walk — it cares
about the objects, not the printed theory summary.

We checked the obvious alternatives to patching, and none fit a 9.2+22164 toolchain:

candidate	why not
MetaRocq/metacoq#main	has this fix, but is adapted to Rocq master generally — e.g. rocq#22166 makes it destructure Global.force_proof as a triple, while our fork still has the pair. Fails earlier, in template-rocq.
MetaRocq/metacoq#9.2	correct for stock 9.2, so it hits the identical error above.
print-assumptions-fine-grained	has the fix, but tracks Rocq master and is missing rocq#21773 (sort poly cumulativity) plus the 9.2 template fixes we need.
older Rocq revisions	anything predating the signature change can't parse our corpus's Require (safe) files.

Patch authored by @rhaps0dy (Adrià Garriga-Alonso); opened by the Theorem Labs build bot on his
behalf. Compile-verified against our fork: the full metacoq chain including
rocq-metarocq-safechecker-plugin.1.5.1+9.2 installs cleanly.