diff options
| author | Hugo Herbelin | 2020-10-19 10:37:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-17 16:19:39 +0100 |
| commit | 73a2675e35b25c65582c02516943b0dd010016dd (patch) | |
| tree | 242b5185a938c996a379838c554cdc537bc36365 | |
| parent | 5e87ba237e2219527095de0aba8744e5c791ac85 (diff) | |
Adding change log for #12984.
Co-authored-by: Ralf Jung <post@ralfj.de>
| -rw-r--r-- | doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst new file mode 100644 index 0000000000..d472e6fdf0 --- /dev/null +++ b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst @@ -0,0 +1,12 @@ +- **Changed:** + Redeclaring a notation reactivates also its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes of behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + <https://github.com/coq/coq/pull/12986>`_ of a priority given to + notations which match a larger part of the term to print + (`#12984 <https://github.com/coq/coq/pull/12984>`_, + fixes `#7443 <https://github.com/coq/coq/issues/7443>`_ + and `#10824 <https://github.com/coq/coq/issues/10824>`_, + by Hugo Herbelin). |