fsf emacs compatibilty for symbol-at-point.

2 files changed, 5 insertions, 4 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 6db1688f..a96cc1a0 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -129,7 +129,7 @@ detect if they start something or not."
 
 
 (defun coq-find-command-end (direction)
-  "Moves to the first end of command found looking at direction.  The opint is put exactly before the last \".\" of the ending token.  If no end command is found, go as far as possible and return nil."
+  "Moves to the first end of command found looking at direction.  The point is put exactly before the last \".\" of the ending token.  If no end command is found, go as far as possible and return nil."
   (if (< direction 0)
       (coq-find-command-end-backward)
     (coq-find-command-end-forward)))
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."