aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-10 11:47:45 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-12-10 11:47:45 +0000
commit9bc3f266832ec50c30802f60e4af5ef88aeadc69 (patch)
treee66da819d249c050d39ea219e724cd15a11aef52 /coq
parent95e2a29f51fb86ee958a261ac195d7e8c96d1741 (diff)
Emacs compatibility/API updates: string-to-int -> string-to-number
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 442ce049..68ea9bc1 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -605,7 +605,7 @@ happen since one of them is necessarily set to t in coq-syntax.el."
((looking-at "subgoal \\([0-9]+\\) is:\n")
(goto-char (match-end 0))
(cons 'goal (match-string 1))
- (setq coq-current-goal (string-to-int (match-string 1))))
+ (setq coq-current-goal (string-to-number (match-string 1))))
((looking-at proof-shell-assumption-regexp)
(cons 'hyp (match-string 1)))
(t nil)))