From 6da3091bdb249af11302042e7958f87b2cd36e63 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Oct 2019 11:46:59 +0200
Subject: Document the ability to bind notation arguments in Ltac2.

---
 doc/sphinx/proof-engine/ltac2.rst | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

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
 *****************
 
-- 
cgit v1.2.3