diff options
author | 2011-07-16 20:35:26 +0000 | |
---|---|---|
committer | 2011-07-16 20:35:26 +0000 | |
commit | 3c0fa55426e61884a8a67661025cc7a32ecc77ac (patch) | |
tree | f5eb4d705e49b103cea10a883e5c1c583d4c41c9 /doc | |
parent | bb7d7b4c22fbe037781b2418002efe09d6c3a409 (diff) |
This adds two option tables 'Printing Record' and 'Printing Constructor'
that forces a given type to always be printed as a record, or with a
constructor, regardless of the setting of 'Printing Records'.
And this is that patch that controls printing by type.
(patch from Tom Prince)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
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 182a50959..3429bafab 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. |