Adding change log for coq#17123

herbelin · Feb 4, 2023 · 0d8080c · 0d8080c
1 parent a3d13c6
commit 0d8080c
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/...g/03-notations/17123-master+support-for-string-constant-tokens-in-notations.rst b/...g/03-notations/17123-master+support-for-string-constant-tokens-in-notations.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Strings can be used as symbols in notations; double quotes can be
+  used in symbols in :g:`only printing` notations; see :ref:`Basic notations <BasicNotations>`
+  for details (`#17123 <https://github.com/coq/coq/pull/17123>`_, by Hugo
+  Herbelin).