aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-syn.tex8
1 files changed, 8 insertions, 0 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 95f3d806b..9f4e45830 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -221,6 +221,14 @@ The command to display the current state of the {\Coq} term parser is
\tt Print Grammar constr.
\end{quote}
+\variant
+
+\comindex{Print Grammar pattern}
+{\tt Print Grammar pattern.}\\
+
+This displays the state of the subparser of patterns (the parser
+used in the grammar of the {\tt match} {\tt with} constructions).
+
\subsection{Displaying symbolic notations}
The command \texttt{Notation} has an effect both on the {\Coq} parser and