diff options
| author | Pierre-Marie Pédrot | 2019-06-09 12:19:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:38:35 +0200 |
| commit | e5c788f9efce9a9dd11910cd53c4a99451c48d8a (patch) | |
| tree | 0ef48e2c5e135bc209ffa036454dfe3c760d2046 /doc | |
| parent | 3d9f2d1cbc6256c48523db00fa2cc9743a843dfe (diff) | |
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.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 8 |
1 files changed, 5 insertions, 3 deletions
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 +++++++++++++ |