diff options
| -rw-r--r-- | coq/coq-indent.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 7 |
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))) @@ -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." |