diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 36eeff6192..3812fd7631 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -850,8 +850,15 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. -Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited -to the use of standalone function calls. +Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can +be done via an explicit annotation to the :n:`ltac1` quotation. + +.. productionlist:: coq + ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) + +The identifiers must be bound in the surrounding Ltac2 environment to values of +type `Ltac2.Ltac1.t` (see below). This syntax will make them available to the +quoted Ltac1 code as if they had been bound from Ltac1 itself. Low-level API +++++++++++++ @@ -869,6 +876,9 @@ focus is very hard. This is why some functions return a continuation-passing style value, as it can dispatch dynamically between focused and unfocused behaviour. +The same mechanism for explicit binding of variables as described in the +previous section applies. + Ltac2 from Ltac1 ~~~~~~~~~~~~~~~~ |