diff options
Diffstat (limited to 'coq/coq-db.el')
| -rw-r--r-- | coq/coq-db.el | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq-db.el b/coq/coq-db.el index 65df920e..cf14c1cd 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -56,12 +56,12 @@ Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a new keyword to colorize." ) -(defun coq-insert-from-db (db) +(defun coq-insert-from-db (db prompt) "Ask for a keyword, with completion on keyword database DB and insert. Insert corresponding string with holes at point. If an insertion function is present for the keyword, call it instead. see `coq-syntax-db' for DB structure." - (let* ((tac (completing-read "tactic (tab for completion) : " + (let* ((tac (completing-read (concat prompt " (tab for completion) : ") db nil nil)) (infos (cddr (assoc tac db))) (s (car infos)) ; completion to insert |