blob: 5c81efa8b96434f433b91ebcb02e443e84855dc4 (
plain)
1
2
3
4
5
6
7
|
- **Fixed:**
Fix an incompleteness in the typechecking of `match` for
cumulative inductive types. This could result in breaking subject
reduction.
(`#13501 <https://github.com/coq/coq/pull/13501>`_,
fixes `#13495 <https://github.com/coq/coq/issues/13495>`_,
by Matthieu Sozeau).
|
