Skip to content

Coq 8.15.1
Compare
Choose a tag to compare
@SkySkimmer SkySkimmer released this 22 Mar 16:36
· 7264 commits to master since this release
V8.15.1
This tag was signed with the committer’s verified signature.
SkySkimmer Gaëtan Gilbert
GPG key ID: 8585BE5E6C57C806
Learn about vigilant mode.
50a980d

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.

Assets 3
Loading