From c71fca0c5ed83ff6995ba3dca6afd398829a114e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Jul 2006 16:30:05 +0000
Subject: Doc Print Grammar pattern

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9007 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-syn.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 95f3d806b0..9f4e458300 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
-- 
cgit v1.2.3