From 9f04be1212d6fd48a12651e828070040a90772a2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 30 Sep 2005 10:25:22 +0000
Subject: Add more user preferences, fix existing ones.

---
 coq/coq.el | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index e6bac99d..1976ac28 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1063,11 +1063,19 @@ Group number 1 matches the name of the library which is required.")
 ;  :type 'boolean
 ;  :setting ("Focus. " . "Unfocus. "))
 
+
+;; FIXME: to handle "printing all" properly, we should change the state
+;; of the variables that also depend on it.
 (defpacustom print-fully-explicit nil
   "*Print fully explicit terms."
   :type 'boolean
   :setting ("Set Printing All. " . "Unset Printing All. "))
 
+(defpacustom print-implicit nil
+  "*Print implicit arguments in applications."
+  :type 'boolean
+  :setting ("Set Printing Implicit. " . "Unset Printing Implicit. "))
+
 (defpacustom print-coercions nil
   "*Print coercions."
   :type 'boolean
@@ -1076,8 +1084,17 @@ Group number 1 matches the name of the library which is required.")
 (defpacustom print-match-wildcards t
   "*Print underscores for unused variables in matches."
   :type 'boolean
-  :setting ("Set Printing Coercions. " . "Unset Printing Coercions. "))
+  :setting ("Set Printing Wildcard. " . "Unset Printing Wildcard. "))
+
+(defpacustom print-elim-types t
+  "*Print synthesised result type for eliminations."
+  :type 'boolean
+  :setting ("Set Printing Synth. " . "Unset Printing Synth. "))
 
+(defpacustom printing-depth 50
+  "*Depth of pretty printer formatting, beyond which dots are displayed."
+  :type 'integer
+  :setting "Set Printing Depth %i. ")
 
 (defpacustom time-commands nil
   "*Whether to display timing information for each command."
-- 
cgit v1.2.3