Documenting use of primitive entry names for restricting syntax in notations.

1 files changed, 25 insertions, 0 deletions

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index da6028126b..a4ed2134e1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -658,6 +658,7 @@ subexpressions occurring in binding position and parsed as terms to be
 {\tt as ident}.
 
 \subsubsection{Binders not bound in the notation}
+\label{NotationsWithBinders}
 
 We can also have binders in the right-hand side of a notation which
 are not themselves bound in the notation. In this case, the binders
@@ -804,6 +805,30 @@ Notation "'exists_non_null' x .. y  , P" :=
   (at level 200, x binder).
 \end{coq_example*}
 
+\subsection{Predefined entries}
+
+By default, sub-expressions are parsed as terms and the corresponding
+grammar entry is called {\tt constr}. However, one may sometimes want
+to restrict the syntax of terms in a notation. For instance, the
+following notation will accept to parse only global reference in
+position of {\tt x}:
+
+\begin{coq_example*}
+Notation "'apply' f a1 .. an" := (.. (f a1) .. an)
+  (at level 10, f global, a1, an at level 9).
+\end{coq_example*}
+
+In addition to {\tt global}, one can restrict the syntax of a
+sub-expression by using the entry names {\tt ident} or {\tt pattern}
+already seen in Section~\ref{NotationsWithBinders}, even when the
+corresponding expression is not used as a binder in the right-hand
+side. E.g.:
+
+\begin{coq_example*}
+Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an)
+  (at level 10, f ident, a1, an at level 9).
+\end{coq_example*}
+
 \subsection{Summary}
 
 \paragraph{Syntax of notations}