From 838cbe33a5caf6a1cad7372be249293103d87828 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 14 Sep 2004 07:57:31 +0000 Subject: Add spaces after setting commands to separate. Temporarily disable print-only-first-subgoal. --- coq/coq.el | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index 9cb6de05..9bdee65b 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -907,25 +907,28 @@ Group number 1 matches the name of the library which is required.") ;; These appear on the Coq -> Setting menu. ;; -(defpacustom print-only-first-subgoal nil - "Whether to just print the first subgoal in Coq." - :type 'boolean - :setting ("Focus. " . "Unfocus. ")) +; FIXME da: we should send this command only inside a proof, +; otherwise it gives an error message. It should be on +; a different menu command. +;(defpacustom print-only-first-subgoal nil +; "Whether to just print the first subgoal in Coq." +; :type 'boolean +; :setting ("Focus. " . "Unfocus. ")) (defpacustom print-fully-explicit nil "*Print fully explicit terms." :type 'boolean - :setting ("Set Printing All." . "Unset Printing All.")) + :setting ("Set Printing All. " . "Unset Printing All. ")) (defpacustom print-coercions nil "*Print coercions." :type 'boolean - :setting ("Set Printing Coercions." . "Unset Printing Coercions.")) + :setting ("Set Printing Coercions. " . "Unset Printing Coercions. ")) (defpacustom print-match-wildcards t "*Print underscores for unused variables in matches." :type 'boolean - :setting ("Set Printing Coercions." . "Unset Printing Coercions.")) + :setting ("Set Printing Coercions. " . "Unset Printing Coercions. ")) (defpacustom time-commands nil -- cgit v1.2.3