diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-12 13:32:34 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-12 13:32:34 +0200 |
| commit | b6b38b7b8865b1d86da49369956e32d2130c7f2c (patch) | |
| tree | 6ae966f4a933c279dd96adf71f76d53389881085 /coq/coq.el | |
| parent | 574b0992e3cb4b7a4ad88400b9a5ab0198a96ca5 (diff) | |
temporary fix of automatic intros.
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -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") |