diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-12 07:29:52 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-02-12 07:29:52 +0100 |
commit | e2dca0d78482e9d1e067e4d0ff847a2b65867498 (patch) | |
tree | 2c865465e8d0b225dd3409eab608c29be97a249b /doc | |
parent | b8efac9f2cadbc0f700408fcb6f8187ef6527fd9 (diff) |
Make clearer that "Remove Printing Let" does not influence destructuring let.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-ext.tex | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 1eb40cd36..71eb0108d 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -560,8 +560,7 @@ The default is to not print synthesizable types. \comindex{Print Table Printing Let}} If an inductive type has just one constructor, -pattern-matching can be written using {\tt let} ... {\tt :=} -... {\tt in}~... +pattern-matching can be written using the first destructuring let syntax. \begin{quote} {\tt Add Printing Let {\ident}.} @@ -572,7 +571,10 @@ pattern-matching is written using a {\tt let} expression. \begin{quote} {\tt Remove Printing Let {\ident}.} \end{quote} -This removes {\ident} from this list. +This removes {\ident} from this list. Note that removing an inductive +type from this list has an impact only for pattern-matching written using +\texttt{match}. Pattern-matching explicitly written using a destructuring +let are not impacted. \begin{quote} {\tt Test Printing Let for {\ident}.} @@ -630,13 +632,19 @@ it is sensible to the command {\tt Reset}. This example emphasizes what the printing options offer. \begin{coq_example} +Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. Test Printing Let for prod. -Print fst. +Print snd. Remove Printing Let prod. Unset Printing Synth. Unset Printing Wildcard. -Print fst. +Print snd. \end{coq_example} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} % \subsection{Still not dead old notations} |