doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst


1
2
3
4
5
6

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