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)
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)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;