[Ltac2] Interpretation scopes in “constr” arguments of tactic notations

2 files changed, 12 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).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 5f2e911ff9..36eeff6192 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -655,6 +655,8 @@ this features has the same semantics as in Ltac1. In particular, a ``reverse``
 flag can be specified to match hypotheses from the more recently introduced to
 the least recently introduced one.
 
+.. _ltac2_notations:
+
 Notations
 ---------
 
@@ -679,6 +681,11 @@ The following scopes are built-in.
 
   + parses :n:`c = @term` and produces :n:`constr:(c)`
 
+  This scope can be parameterized by a list of delimiting keys of interpretation
+  scopes (as described in :ref:`LocalInterpretationRulesForNotations`),
+  describing how to interpret the parsed term. For instance, :n:`constr(A, B)`
+  parses :n:`c = @term` and produces :n:`constr:(c%A%B)`.
+
 - :n:`ident`:
 
   + parses :n:`id = @ident` and produces :n:`ident:(id)`