- more info on the elements of proof-action-list; the COMMANDS

  list in it should be concatenated with (mapconcat 'identity
  COMMANDS " "), which is not the case proof-shell-insert.

1 files changed, 1 insertions, 2 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 91e5768f..255ca23f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1668,8 +1668,7 @@ compilation (if necessary) of the dependencies."
             (coq-object-hash-symbol nil)
             string)
         (dolist (item queueitems)
-          (let (;; XXX car or concat ?
-                (string (car (nth 1 item))))
+          (let ((string (mapconcat 'identity (nth 1 item) " ")))
             (when (and string
                        (string-match coq-require-command-regexp string))
               (let ((span (car item))