Repository navigation

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