diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 182a50959a..3429bafabf 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -200,10 +200,19 @@ Definition b := {| x := 5; y := 3 |}. Definition c := {| y := 3; x := 5 |}. \end{coq_example} -This syntax can be disabled for printing by +This syntax can be disabled globally for printing by \begin{quote} {\tt Unset Printing Records.} \end{quote} +For a given type, one can override this using either +\begin{quote} +{\tt Add Printing Record {\ident}.} +\end{quote} +to get record syntax or +\begin{quote} +{\tt Add Printing Constructor {\ident}.} +\end{quote} +to get constructor syntax. This syntax can also be used for pattern matching. |