From 6ba98422a95a799778378ecf7e34febc6577fa3b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 24 Aug 2010 13:02:12 +0000
Subject: proof-script-command-end-regexp: allow any non-letter after a period
 to terminate a command, fixing #296 (and hopefully not messing up other
 cases).

---
 coq/coq.el          | 2 +-
 etc/trac/trac-296.v | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index 3817c5a3..3f4fff4c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -650,7 +650,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-\\|\\'\\)")
+        "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|[^[:alpha:]]\\)")
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
   (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name
diff --git a/etc/trac/trac-296.v b/etc/trac/trac-296.v
index ac0e223f..4ac6a676 100644
--- a/etc/trac/trac-296.v
+++ b/etc/trac/trac-296.v
@@ -1,3 +1,6 @@
 (* PG accepts this as valid though it isn't;
    see http://proofgeneral.inf.ed.ac.uk/trac/ticket/296 *)
 Check nat.&!&*\:,.:<*&!)@)$.
+
+(* How should this one parse? *)
+Check 0.99.
-- 
cgit v1.2.3