Repository navigation

Support for Rocq/Coq 9.0 - #547

Merged

xavierleroy merged 9 commits into

May 5, 2025

Merged

Support for Rocq/Coq 9.0#547
xavierleroy merged 9 commits into
masterfrom
coq-9.0

Commits on May 5, 2025
- Add explicit interface for backend/Inliningaux
  xavierleroy
  committed
  829fe1b
- Update vendored Flocq to 4.2.1
  xavierleroy
  committed
  06025bd
- Update supported Coq/Rocq version numbers
  xavierleroy
  committed
  794ae82
- Turn warning "unused-case" off for OCaml files extracted from Coq
  xavierleroy
  committed
  3d0521b
- Tweak warning options for Coq/Rocq 9.0
  xavierleroy
  committed
  7ee9021
- Add `From Coq` to `Require` of standard library modules
  xavierleroy
  committed
  5e4ef44
- CI action `oldest` updated to Coq 8.15
  xavierleroy
  committed
  2105e81
- CI action `latest` updated to Rocq 9.0
  xavierleroy
  committed
  5d2f6b8
- Update tests
  xavierleroy
  committed
  86162b0