rocq-prover/rocq V8.15.1

Coq 8.15.1

on GitHub

Main fixes:

• inconsistency with module subtyping and inductive types (#15838)
• CoqIDE slowdown on large files
• missing .vok file creation
• cbn regression (#15567)
• usability of schemes with elim foo using scheme with (P0 := ...) (the P0 name was not accessible in 8.15.0) (#15420)

See the changelog for detailed changes.