From da2d9cd4b532824e23deaaed7704c5bb8a94ac1c Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Thu, 12 Feb 2026 10:40:33 +0100 Subject: [PATCH 1/2] Add support for 'repeat-mode' --- generic/proof-menu.el | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/generic/proof-menu.el b/generic/proof-menu.el index f9801bbae..e591162e8 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -143,6 +143,15 @@ without adjusting window layout." ;; NB: C-c ` is next-error in universal-keys (proof-define-keys map proof-universal-keys)) +(defvar proof-repeat-map + (let ((map (make-sparse-keymap))) + (define-key map (kbd "C-n") #'proof-assert-next-command-interactive) + (define-key map (kbd "C-u") #'proof-undo-last-successful-command) + map)) + +;; support for `repeat-mode' (≥Emacs 28) +(put #'proof-assert-next-command-interactive 'repeat-map 'proof-repeat-map) +(put #'proof-undo-last-successful-command 'repeat-map 'proof-repeat-map) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; From 0c4df8ad38e3bd697f179f276aeb9a2b4e81d7d0 Mon Sep 17 00:00:00 2001 From: Philip Kaludercic Date: Fri, 13 Feb 2026 09:21:21 +0100 Subject: [PATCH 2/2] Inherit input-method when asking user * coq.el (coq-guess-or-ask-for-string): Pass a non-nil value for INHERIT-INPUT when invoking 'read-string'. --- coq/coq.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/coq.el b/coq/coq.el index f9b25eae2..7f3c92f39 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -961,7 +961,7 @@ Otherwise propose identifier at point if any." (t (coq-id-or-notation-at-point))))) (read-string (if guess (concat s " (default " guess "): ") (concat s ": ")) - nil 'proof-minibuffer-history guess))) + nil 'proof-minibuffer-history guess t))) (defun coq-ask-do (ask do &optional dontguess postformatcmd wait)