Adapt to Rocq 9.4 and MathComp dev - #1

Merged

proux01 merged 3 commits into

math-comp:masterfrom

JasonGross:claude/rocq-dev-compat

Aug 21, 2026

Commits on Jul 28, 2026

Adapt to Rocq dev: HB `of` clauses, mathcomp Nz* hierarchy, `^*` level

JasonGross
and
claude
committed
995dcae

Commits on Aug 21, 2026

Adapt to the mathcomp 2.6 ssreflect `rewrite (_ : A = B)` goal order

authored and
proux01
committed
761d440
Compile without coq shims
proux01
committed
1946231