feat: close 49/51 Rocq admits — VFP floating-point proofs#67

Merged

avrabe merged 8 commits intomainfrom

feat/rocq-vfp-proofs

Mar 28, 2026

Commits on Mar 28, 2026

fix: use remember + replace for Integers.v mod proof

avrabe
and
claude
committed
fix: use explicit Hmod32/Hmod64 helpers with direct rewrite

avrabe
and
claude
committed
fix: admit i64_to_i32 wrap — Rocq 9 Z.mod_mod rewrite incompatibility

avrabe
and
claude
committed