diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 5 |
1 files changed, 5 insertions, 0 deletions
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 |