From ecd39d515ef6a92c8202d90e27456994dcbb87b4 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 5 Mar 2018 13:57:39 -0500 Subject: [PATCH] alway put newline after conclusion --- coq/coq-goals.el | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/coq/coq-goals.el b/coq/coq-goals.el index 149999582..2a32f5b7c 100644 --- a/coq/coq-goals.el +++ b/coq/coq-goals.el @@ -140,8 +140,7 @@ (insert (coq-goals--format-goal-with-hypotheses (coq-goals--goal-goal goal1) (coq-goals--goal-hypotheses goal1))) - (when goals-rest - (insert "\n"))) + (insert "\n")) (dolist (goal goals-rest) (cl-incf goal-counter) (insert (format "\nsubgoal %s (ID %s):\n" goal-counter (coq-goals--goal-id goal))) @@ -170,7 +169,7 @@ (beginning-of-line) ;; find something backward else than a space: end of conclusion (ignore-errors (search-backward-regexp "\\S-")) - (recenter (- 1)) ; put bottom of conclusion at bottom of window + (recenter -1) ; put bottom of conclusion at bottom of window (beginning-of-line) ;; if the top of conclusion is hidden we may want to show it instead ;; of bottom of conclusion