diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 12:49:37 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 12:49:37 +0000 |
| commit | 86ac9c837f694cc2ce1849a6b839215e929e0d55 (patch) | |
| tree | 114479e89b0161a39ebb6ca1e8de044ca6db867b /coq/coq-db.el | |
| parent | 62dacef3e83b2b95068337ba894c89176265cc09 (diff) | |
Small fixes.
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 |