diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_declare.ml | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 16 |
2 files changed, 19 insertions, 9 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index eb8161c2bb..68ae5628db 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,14 +1,12 @@ -let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let declare_definition ~poly ident sigma body = - let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ident k ~opaque:false sigma udecl body None [] - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 36eeff6192..3036648b08 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -850,8 +850,17 @@ 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 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 +++++++++++++ @@ -869,6 +878,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 ~~~~~~~~~~~~~~~~ |