From 44ff04eef9a3c1c9e499eb9f1c98db0765cdabb4 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 25 Aug 2010 08:18:59 +0000 Subject: Revert 10.51. proof-script-command-end-regexp: non-letters after periods are used in some notations (e.g. SSReflect). See Trac #296. --- coq/coq.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/coq.el b/coq/coq.el index 75913a71..e2e4c4ba 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -653,7 +653,7 @@ This is specific to `coq-mode'." (set (make-local-variable 'indent-tabs-mode) nil) (setq proof-terminal-char ?\.) (setq proof-script-command-end-regexp - "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|[^[:alpha:]]\\|\\'\\)") + "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)") (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name -- cgit v1.2.3