Skip to content

Commit

Permalink
Fixing #485, bug on proof without "Proof".
Browse files Browse the repository at this point in the history
Due to a re-search that should fail silently.
  • Loading branch information
Matafou committed May 4, 2020
1 parent 84b81a8 commit 23db83d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion coq/coq.el
Original file line number Diff line number Diff line change
Expand Up @@ -2661,7 +2661,7 @@ built from the list of strings in SUGGESTED."
(with-current-buffer proof-script-buffer
(save-excursion
(goto-char (span-start span))
(let* ((endpos (re-search-forward coq-proof-using-regexp)))
(let* ((endpos (re-search-forward coq-proof-using-regexp (span-end span) t)))
(when endpos
(let* ((suggested (span-property span 'dependencies))
(proof-pos (match-beginning 0))
Expand Down

0 comments on commit 23db83d

Please sign in to comment.