diff options
| author | Théo Zimmermann | 2019-11-27 20:29:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-27 20:29:29 +0100 |
| commit | ac99c6aba0091d5c1ee9511508e25d399425b61b (patch) | |
| tree | d21fb562b7a6f73b00f803909e2ecf181da4aa50 | |
| parent | 353b601323ffd7d5b4acc3c02de985b27cddc8e5 (diff) | |
| parent | 597a8a0e0f1bc50a0f1eb5fbdce52881df14aada (diff) | |
Merge PR #11199: Correcting unintended changelog message for #11090 (coercion+notation regression)
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/changelog/03-notations/11090-master+refactoring-application-printing.rst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst index 5c3936073a..4423c2b587 100644 --- a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst +++ b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst @@ -1 +1,3 @@ -- Fixed #11033: regression in not printing coercions to which is also associated a notation (`#11090 <https://github.com/coq/coq/pull/11090>`_, by Hugo Herbelin). +- Fixed an 8.10 regression related to the printing of coercions associated to notations + (`#11090 <https://github.com/coq/coq/pull/11090>`_, + fixes ` #11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). |