diff options
Diffstat (limited to 'doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst')
| -rw-r--r-- | doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst index fba09f5e87..16ca9caf48 100644 --- a/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst +++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst @@ -1,4 +1,5 @@ -- White spaces are forbidden in the “&ident” syntax for ltac2 references +- **Changed:** + White spaces are forbidden in the :n:`&@ident` syntax for ltac2 references that are described in :ref:`ltac2_built-in-quotations` (`#10324 <https://github.com/coq/coq/pull/10324>`_, fixes `#10088 <https://github.com/coq/coq/issues/10088>`_, |