diff options
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-syn.tex | 8 |
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 |