diff options
| author | Vincent Laporte | 2019-06-04 12:57:16 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-06-06 08:39:18 +0000 |
| commit | fe49db8833803f87e2f750b698f28868d276bfe6 (patch) | |
| tree | 70a687a0cbf4b9ea3954bf6892383f4e26282237 /doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst | |
| parent | 4f7af2b09a935528d660a354f5e7672fc92e9a5c (diff) | |
[Ltac2] Interpretation scopes in “constr” arguments of tactic notations
Diffstat (limited to 'doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst')
| -rw-r--r-- | doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst new file mode 100644 index 0000000000..bd1c0c42e8 --- /dev/null +++ b/doc/changelog/05-tactic-language/10289-ltac2+delimited-constr-in-notations.rst @@ -0,0 +1,5 @@ +- Ltac2 tactic notations with “constr” arguments can specify the + interpretation scope for these arguments; + see :ref:`ltac2_notations` for details + (`#10289 <https://github.com/coq/coq/pull/10289>`_, + by Vincent Laporte). |