diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-16 20:35:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-16 20:35:26 +0000 |
| commit | 3c0fa55426e61884a8a67661025cc7a32ecc77ac (patch) | |
| tree | f5eb4d705e49b103cea10a883e5c1c583d4c41c9 /tools/coq-syntax.el | |
| 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 'tools/coq-syntax.el')
| -rw-r--r-- | tools/coq-syntax.el | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el index bc0e18e57..8630fb3a9 100644 --- a/tools/coq-syntax.el +++ b/tools/coq-syntax.el @@ -417,8 +417,10 @@ ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") + ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") + ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") |