Documenting the Ltac2 change.

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
 ~~~~~~~~~~~~~~~~