diff options
| author | coqbot-app[bot] | 2020-09-28 16:18:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-28 16:18:52 +0000 |
| commit | 982c28216f3eb49abfd6b97c69b8fc116c813117 (patch) | |
| tree | 47edf047d93d4ead9d52afc795c812c34063a503 /doc | |
| parent | bd24f72a06343b375ad20aaa5b7296c2ad904a5c (diff) | |
| parent | a0090dc6930c1f0c60ca6144d1551019ecbcc837 (diff) | |
Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lonely notation at printing time.
Reviewed-by: ejgallego
Ack-by: maximedenes
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst new file mode 100644 index 0000000000..95a9093272 --- /dev/null +++ b/doc/changelog/03-notations/12946-master+fix12908-part1-collision-lonely-notation-printing.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Undetected collision between a lonely notation and a notation in + scope at printing time + (`#12946 <https://github.com/coq/coq/pull/12946>`_, + fixes the first part of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). |