Merge PR#485: Document Show Match

2 files changed, 18 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1d423f8b16..1860c0465c 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -651,6 +651,11 @@ Print snd.
 Reset Initial.
 \end{coq_eval}
 
+\subsection{Printing \mbox{\tt match} templates}
+
+The {\tt Show Match} vernacular command prints a {\tt match} template for
+a given type. See Section~\ref{Show}.
+
 % \subsection{Still not dead old notations}
 
 % The following variant of {\tt match} is inherited from older version
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 16c822b6a5..6d54b4de15 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -492,6 +492,19 @@ process of an {\tt intros}.
 the set of all uninstantiated existential variables in the current proof tree, 
 along with the type and the context of each variable.
 
+\item{\tt Show Match {\ident}.\label{ShowMatch}}\comindex{Show Match}\\
+This variant displays a template of the Gallina {\tt match} construct 
+with a branch for each constructor of the type {\ident}.
+
+Example:
+
+\begin{coq_example}
+Show Match nat.  
+\end{coq_example}
+\begin{ErrMsgs}
+\item \errindex{Unknown inductive type}
+\end{ErrMsgs}
+
 \item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
 \\ It displays the set of all universe constraints and its
 normalized form at the current stage of the proof, useful for