Rocq 9.1 upgrade blocked by universe constraint error in RocqOfRust/M.v

[avrabe]

Problem

Upgrading from Rocq 9.0 to 9.1 fails when compiling RocqOfRust/M.v (from upstream rocq-of-rust):

File "./RocqOfRust/M.v", line 20, characters 0-91:
Error: Missing universe constraint declared for inductive type:
Type@{RocqOfRust.M.22} <= Set

Rocq 9.1 tightened universe constraint checking with -impredicative-set. The upstream M.v file needs explicit universe annotations to be compatible.

Affected component

Upstream: formal-land/rocq-of-rust — RocqOfRust/M.v

What works

All other dependencies are ready for 9.1 in nixpkgs:

• rocq-core 9.1.1 ✅
• coq-hammer 1.3.2+9.1 ✅
• coqutil 0.0.7 (supports 9.0–9.2) ✅
• smpl rocq-9.0 branch (declares rocq-core >= 9.0) ✅ — fixed to build against matching version

Draft PR

#30 has the upgrade work ready (including smpl version-matching fix). Marked as draft until upstream resolves the universe constraint issue.

Next steps

• Report upstream at formal-land/rocq-of-rust
• Monitor for a rocq-of-rust commit that supports Rocq 9.1
• Once upstream fixes M.v, rebase chore: upgrade Rocq 9.0 → 9.1 #30 and merge