From 23db83dc4141d89530f6381ba49f56399682d4e0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 4 May 2020 14:40:59 +0200
Subject: Fixing #485, bug on proof without "Proof".

Due to a re-search that should fail silently.
---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index cb43f3a9..ca1e36a1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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))
-- 
cgit v1.2.3