From dab51c396e16fdcf8b96093c33feb2f67c53d94d Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 17 Mar 2017 15:35:50 -0400
Subject: Document Show Match, add ref to that in match variants/extensions

---
 doc/refman/RefMan-ext.tex |  5 +++++
 doc/refman/RefMan-pro.tex | 13 +++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233c..03fe92c772 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
-- 
cgit v1.2.3