diff options
| author | Emilio Jesus Gallego Arias | 2020-06-01 16:36:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-01 16:36:44 +0200 |
| commit | 558e20c25d2e030d4ba4a0b42458969564815223 (patch) | |
| tree | 233d672aa44ea749f96cea01c414c736d6db403a /doc | |
| parent | 4270ed35f2a26f226b01f2293f61d18773e6260b (diff) | |
| parent | dec5edf7c92950881693afe2040d711155cf15b5 (diff) | |
Merge PR #12422: Fixes #12418: an assert false in inference of return clause
Reviewed-by: gares
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst new file mode 100644 index 0000000000..8f126c5b6f --- /dev/null +++ b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match` + (`#12422 <https://github.com/coq/coq/pull/12422>`_, + fixes `#12418 <https://github.com/coq/coq/pull/12418>`_, + by Hugo Herbelin). |