diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 7 |
1 files changed, 7 insertions, 0 deletions
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)` |