From 3c0fa55426e61884a8a67661025cc7a32ecc77ac Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Jul 2011 20:35:26 +0000
Subject: 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
---
 tools/coq-syntax.el | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tools')

diff --git a/tools/coq-syntax.el b/tools/coq-syntax.el
index bc0e18e570..8630fb3a9c 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")
-- 
cgit v1.2.3