Coq 8.19.1

The tag for 8.19.1 has been set to commit 8152d125abb0fb7e8cbecf4bd6cd51d8d3e70d78.

Coq 8.19.1 fixes a number of bugs, most notably:

- incorrect abstraction of sort variables for opaque constants leading to an inconsistency (Missing abstraction of const_relevance for opaques (Anomaly "File "kernel/cClosure.ml", line 138, characters 6-12: Assertion failed.") · Issue #18594 · coq/coq · GitHub)

- memory corruption with vm_compute (rare but more likely with OCaml 5.1) (Stash the bytecode interpreter's internal structures when OCaml's runtime is processing a signal. by silene · Pull Request #18599 · coq/coq · GitHub)

See changelog for details: Recent changes — Coq 8.20+alpha documentation

1 Like