From 51dc54951ae03373c25782af6cbce4fe0c2f9493 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon@bedrocksystems.com>
Date: Mon, 23 May 2022 12:50:41 -0400
Subject: [PATCH 1/2] add customizable variables to configure which part of a
 goal the goal buffer will focus on

---
 coq/coq.el | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 34ea72c0b..080c0a1ef 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -115,6 +115,18 @@ Namely, goals that do not fit in the goals window."
   :type 'boolean
   :group 'coq)
 
+(defcustom coq-goal-conclusion-marker "========"
+  "Marks the part of interest in each goal to focus the goal buffer on"
+  :type regexp
+  :group 'coq
+  )
+
+(defcustom coq-center-goal-after-focus 'top
+  "Where to display the goal marker after rendering a proof goal"
+  :type '(radio
+    (const :tag "move conclusion marker to the top of the window" top)
+    (const :tag "move conclusion marker to the middle of the window" middle)
+    (const :tag "move conclusion marker to the bottom of the window" bottom)))
 
 (defconst coq-shell-init-cmd
   (append
@@ -3163,7 +3175,10 @@ buffer."
           (goto-char (match-beginning 0))
           (buffer-substring p (point)))))))
 
-
+(defun coq-recenter-goal (loc)
+  (cond ((eq loc 'top) (recenter 0))
+        ((eq loc 'middle) (recenter nil))
+        ((eq loc 'bottom) (recenter -1))))
 
 (defun coq-show-first-goal ()
   "Scroll the goal buffer so that the first goal is visible.
@@ -3192,10 +3207,11 @@ number of hypothesis displayed, without hiding the goal"
                 ;; if the top of concl is hidden we may want to show it instead
                 ;; of bottom of concl
                 (when (and coq-prefer-top-of-conclusion
-                         ;; return nil if === is not visible
-                         (not (save-excursion (re-search-backward "========" (window-start) t))))
-                  (re-search-backward "========" nil t)
-                  (recenter 0))
+                           ;; return nil if conclusion marker is not visible
+                           (not (save-excursion (re-search-backward coq-goal-conclusion-marker
+                                                                    (window-start) t))))
+                  (re-search-backward coq-goal-conclusion-marker nil t)
+                  (coq-recenter-goal coq-center-goal-after-focus))
                 (beginning-of-line))))))))
 
 (defvar coq-modeline-string2 ")")

From f35d937e8e450bebdbb8f07765387d065d88af9f Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon.hudon@gmail.com>
Date: Fri, 27 May 2022 14:32:38 -0400
Subject: [PATCH 2/2] Update coq.el

---
 coq/coq.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index 080c0a1ef..f2336c3e9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -117,7 +117,7 @@ Namely, goals that do not fit in the goals window."
 
 (defcustom coq-goal-conclusion-marker "========"
   "Marks the part of interest in each goal to focus the goal buffer on"
-  :type regexp
+  :type 'regexp
   :group 'coq
   )