diff options
Diffstat (limited to 'doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst')
| -rw-r--r-- | doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst deleted file mode 100644 index bf792fda6d..0000000000 --- a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **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). |