aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2012-05-24 12:55:55 +0000
committerGravatar Hendrik Tews <hendrik@askra.de>2012-05-24 12:55:55 +0000
commit445d904669fed7d41b70bdecd268af1935c5f43e (patch)
tree5d78c721f292dea2495aa51a96134fcf4c86c070
parent4634aede2ac4ad03007c0c66bdad8e85215789bd (diff)
fix "Hide Additional Subgoals" for coq 8.4beta
-rw-r--r--coq/coq.el3
1 files changed, 1 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 4ab3f466..98598df1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -176,7 +176,7 @@ On Windows you might need something like:
:type 'string
:group 'coq)
-(defcustom coq-end-goals-regexp-hide-subgoals "\nsubgoal 2 is:"
+(defcustom coq-end-goals-regexp-hide-subgoals "\nsubgoal 2 "
"Regexp for `proof-shell-end-goals-regexp' when hiding additional subgoals.
See also `coq-hide-additional-subgoals'."
:type '(choice regexp (const nil))
@@ -953,7 +953,6 @@ If locked span already has a state number, then do nothing. Also updates
(defun coq-hide-additional-subgoals-switch ()
"Function invoked when the user switches `coq-hide-additional-subgoals'."
- (message "chass")
(if coq-hide-additional-subgoals
(setq proof-shell-end-goals-regexp coq-end-goals-regexp-hide-subgoals)
(setq proof-shell-end-goals-regexp coq-end-goals-regexp-show-subgoals)))