From 243be28e25cfe462034d42f3821cfca9907b3286 Mon Sep 17 00:00:00 2001 From: Dario Halilovic Date: Tue, 17 Feb 2026 15:16:40 +0100 Subject: [PATCH] fix(coq): fix `coq-insert-named-goal-selectors` The move to yasnippet made `coq-insert-named-goal-selectors` raise a "Wrong type argument: string-or-char-p, nil" in the echo area, and also broke indentation. --- coq/coq-abbrev.el | 4 +++- coq/coq.el | 7 ++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index ba10f4421..fd6d7a39a 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -111,7 +111,9 @@ start." (when snippet (if (and coq-use-yasnippet (fboundp 'yas-expand)) (yas-expand-snippet (coq-yas-snippet-from-db snippet)) - (insert (coq-simple-abbrev-from-db snippet))))) + (let ((start (point))) + (insert (coq-simple-abbrev-from-db snippet)) + (indent-region start (point)))))) ;; (if (fboundp 'with-undo-amalgamate) ;; emacs > 29.1 ;; (with-undo-amalgamate (insert abbr) (yas-expand)) diff --git a/coq/coq.el b/coq/coq.el index f9b25eae2..7848c9de3 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2938,13 +2938,10 @@ Goals that are marked as \"only printing\" are ignored." ;; NOTE: Adding braces would be great, but it messes up indentation. (format-selector (lambda (name) (format "[%s]: #." name))) (goal-selectors (cl-mapcar format-selector goal-names)) - (snippet (string-join goal-selectors "\n")) - (snippet (coq-insert-template snippet))) - (message "%s" goal-names) + (snippet (string-join goal-selectors "\n"))) (if (equal goal-selectors nil) (error "Couldn't find any named goals") - (let ((start (point))) - (if coq-use-yasnippet (yas-expand-snippet snippet) (insert snippet)))))))) + (coq-insert-template snippet)))))) (defun coq-insert-match () "Insert a match expression from a type name by Show Match.