diff options
| author | Hugo Herbelin | 2019-12-03 00:47:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-03 01:30:24 +0100 |
| commit | 645447c1e05a95e90d09b946b322a5b587482e8e (patch) | |
| tree | d154e12819fc51590fb63977f937a791cdc6ca14 /doc | |
| parent | be04b1536fe250e8f761701f9e99650bede608d6 (diff) | |
Fixes #11231 (missing dependency in pattern-matching decompilation).
The missing dependency impacted the algorithm for detecting default
clauses.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst new file mode 100644 index 0000000000..ad240ea30b --- /dev/null +++ b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst @@ -0,0 +1,6 @@ +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`, reported by Barry + Jay). |