diff options
| author | Maxime Dénès | 2017-04-07 12:59:01 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-07 12:59:31 +0200 |
| commit | d0f9c9138fdc4cbf88f305ee7fa2395778bdb7cf (patch) | |
| tree | bae453ce1577c6875204b5ceba9f4efd6d1b794f /doc/refman/RefMan-ext.tex | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
| parent | dab51c396e16fdcf8b96093c33feb2f67c53d94d (diff) | |
Merge PR#485: Document Show Match
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 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 |