Record the checks a module operation skipped

[JasonGross]

Print Assumptions reports a definition as closed under the global context when it was built with universe checking off, if a module operation was involved.

Module Type T. Parameter Inline foo : Set. End T.
Module Impl.
  Unset Universe Checking.
  Definition foo : Set := Set.
  Set Universe Checking.
End Impl.
Module F (X : T). Definition foo := X.foo. End F.
Module M := F Impl.
Print Assumptions M.foo.   (* Closed under the global context *)

Four shapes, one cause. The operation either inlines a body someone else checked (Parameter Inline, above, #12155) or runs its own subtyping check (functor application #16646, Include, sealing Module M : T := X). Neither leaves a trace in a declaration: inlining drops the reference to the constant that recorded the skipped check, and a subtyping check belongs to no declaration at all.

Not only universes. The same setup with Unset Guard Checking and a non-terminating Fixpoint makes rocq compile accept and rocqchk reject with Type error: IllFormedRecBody, because the derived constant claims a guard check nobody ran.

Fix

Module bodies get mod_typing_flags: the checks the operation actually performed, i.e. the flags in force for its subtyping checks, met with the flags of every body it inlined. An ordinary module records full checking.

• rocqchk weakens its own re-checking by them at the top of check_module. It has to be the module and not the declarations, because the checker redoes the operation: check_mexpr re-runs check_subtypes for the application, check_module re-compares the result against the stored signature, and neither is attributable to a declaration. CheckFlags.set_local_flags becomes a meet, so an inner declaration cannot ask back for a check the enclosing operation skipped.
• Print Assumptions reports a constant under the flags of the modules it sits in, following the user name — for a sealed module it is the sealing that skipped the check, not the implementation.

Behaviour change: rocqchk now accepts these files and lists the constants under Constants/Inductives relying on type-in-type (or ... unsafe (co)fixpoints), where before it rejected two of the four.

All four check_* travel, check_eliminations included, though nothing can currently set that one.

.vo gains one field on module bodies. vo_magic is derived from the version number, so there is nothing to bump.

Tests

test-suite/output/bug_12155.v for what Print Assumptions says and test-suite/output-coqchk/bug_12155.v for what the checker says, covering the four shapes, the guard case, and one where nothing is recorded. Full test-suite green.

Fixes #12155, fixes #16646.

Turned up on the way, unrelated: rocqchk printed Anomaly "Uncaught exception Modops.ModuleTypingError(_)" for two of these rather than an error message — #22373.

---

Opened autonomously by Claude (Opus 5) on behalf of Jason Gross (jason@theorem.dev).