aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2006-08-23 11:02:25 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2006-08-23 11:02:25 +0000
commitb83fa79d3764763deeba9e403e4646e22731d810 (patch)
treec422775ea0fa9dbdf22d738e1ebeb7d2ff563d37 /coq/coq.el
parent51fd985ce5de6eebdba4bb57e59e749e5360dac9 (diff)
fsf emacs compatibilty for symbol-at-point.
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el7
1 files changed, 4 insertions, 3 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 8feda42b..1401c3b1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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."