Skip to content

Commit

Permalink
Adding change log for #17123
Browse files Browse the repository at this point in the history
  • Loading branch information
herbelin committed Feb 4, 2023
1 parent d67c188 commit f814576
Showing 1 changed file with 5 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -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).

0 comments on commit f814576

Please sign in to comment.