- **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).