- **Added:**
  Inference of return predicate of a :g:`match` by inversion takes
  sort elimination constraints into account
  (`#13290 <https://github.com/coq/coq/pull/13290>`_,
  grants `#13278 <https://github.com/coq/coq/issues/13278>`_,
  by Hugo Herbelin).