diff options
| author | Pierre Courtieu | 2006-08-23 11:02:25 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-08-23 11:02:25 +0000 |
| commit | b83fa79d3764763deeba9e403e4646e22731d810 (patch) | |
| tree | c422775ea0fa9dbdf22d738e1ebeb7d2ff563d37 /coq/coq.el | |
| parent | 51fd985ce5de6eebdba4bb57e59e749e5360dac9 (diff) | |
fsf emacs compatibilty for symbol-at-point.
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -620,16 +620,17 @@ This function calls `coq-find-and-forget-v81' or ) ) + (defun coq-guess-or-ask-for-string (s &optional dontguess) (let ((guess (and (not dontguess) (if (region-exists-p) (buffer-substring-no-properties (region-beginning) (region-end)) - (symbol-near-point))))) + (thing-at-point 'word))))) (read-string (if guess (concat s " (" guess "): ") (concat s " : ")) - nil 'proof-minibuffer-history guess)) - ) + nil 'proof-minibuffer-history guess))) + (defun coq-ask-do (ask do &optional dontguess postformatcmd) "Ask for an ident and print the corresponding term." |
