diff options
| author | Pierre Courtieu | 2021-04-08 16:54:49 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2021-04-08 16:54:49 +0200 |
| commit | d0acb626eba17023c55b002921870d60e48527a5 (patch) | |
| tree | aa853eb90ec1b16f1fcc560cb00f6ff722bbb571 | |
| parent | 5dc5e6f085b1f2b2fb6a2ee6216b6d609310071b (diff) | |
Fixing "match with" generation.
| -rw-r--r-- | coq/coq.el | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -2851,7 +2851,7 @@ Also insert holes at insertion positions." (setq cmd (read-string "Build match for type: ")) (let* ((thematch (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd "."))) - (match (replace-regexp-in-string "=> \n" "=> #\n" thematch))) + (match (replace-regexp-in-string "=> *\n" "=> #\n" thematch))) ;; if error, it will be displayed in response buffer (see def of ;; proof-shell-invisible-cmd-get-result), otherwise: (unless (proof-string-match coq-error-regexp match) |
