From e5c788f9efce9a9dd11910cd53c4a99451c48d8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 9 Jun 2019 12:19:28 +0200
Subject: Give a functional type to Ltac1 quotations with a context.

This looks more principled, and doesn't require as much tinkering with
the typing implementation.
---
 doc/sphinx/proof-engine/ltac2.rst | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3812fd7631..3036648b08 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -856,9 +856,11 @@ 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.
+The return type of this expression is a function of the same arity as the number
+of identifiers, with arguments of type `Ltac2.Ltac1.t` (see below). This syntax
+will bind the variables in the quoted Ltac1 code as if they had been bound from
+Ltac1 itself. Similarly, the arguments applied to the quotation will be passed
+at runtime to the Ltac1 code.
 
 Low-level API
 +++++++++++++
-- 
cgit v1.2.3