diff options
| author | Vincent Laporte | 2019-07-29 13:48:06 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-07-29 14:21:32 +0000 |
| commit | 2802a98273bd1478113130a235bf406d2f7f73f5 (patch) | |
| tree | 2419cffdb0c796fb1f49b2a7ed8ebda84a95ed03 /doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst | |
| parent | b409b9793ba6219053818ac203c95e6bf87f0608 (diff) | |
Document changes by PR 10324
White spaces are forbidden in the “&ident” syntax for ltac2 references.
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 | 5 |
1 files changed, 5 insertions, 0 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 new file mode 100644 index 0000000000..fba09f5e87 --- /dev/null +++ b/doc/changelog/05-tactic-language/10324-ltac2-ssr-ampersand.rst @@ -0,0 +1,5 @@ +- White spaces are forbidden in the “&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>`_, + authored by Pierre-Marie Pédrot). |