diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 18d2c79461..cfdc70d50e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -563,6 +563,20 @@ for it. - `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. +In the special case where Ltac2 antiquotations appear inside a Coq term +notation, the notation variables are systematically bound in the body +of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents +untyped syntactic Coq expressions, which can by typed in the +current context using the `Ltac2.Constr.pretype` function. + +.. example:: + + The following notation is essentially the identity. + + .. coqtop:: in + + Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). + Dynamic semantics ***************** |