From b6b38b7b8865b1d86da49369956e32d2130c7f2c Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 12 May 2017 13:32:34 +0200 Subject: temporary fix of automatic intros. --- coq/coq.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/coq/coq.el b/coq/coq.el index 1bc382ea..45a9a971 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2194,7 +2194,8 @@ mouse activation." (defun coq--format-intros (output) "Create an “intros” form from the OUTPUT of “Show Intros”." - (let* ((shints (replace-regexp-in-string "[\r\n ]*\\'" "" output))) + (let* ((shints1 (replace-regexp-in-string "^[0-9] subgoal\\(.\\|\n\\|\r\\)*" "" output)) + (shints (replace-regexp-in-string "[\r\n ]*\\'" "" shints1))) (if (or (string= "" shints) (string-match coq-error-regexp shints)) (error "Don't know what to intro") -- cgit v1.2.3