diff options
Diffstat (limited to 'doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst')
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 <https://github.com/coq/coq/pull/14093>`_, + fixes `#14092 <https://github.com/coq/coq/issues/14092>`_, + by Pierre-Marie Pédrot). |