From 86ac9c837f694cc2ce1849a6b839215e929e0d55 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 25 Aug 2006 12:49:37 +0000 Subject: Small fixes. --- coq/coq-db.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'coq/coq-db.el') 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 -- cgit v1.2.3