bug fix with terminal regexp (pb with :"unfold foo in |- *.")

3 files changed, 28 insertions, 25 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 7843e529..78f9aea6 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -72,7 +72,7 @@
 		("i" "intro " holes-abbrev-complete 10)
 		("if" "if # then # else #" holes-abbrev-complete 1)
 		("in" "intro" holes-abbrev-complete 1)
-		("inf" "infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1)
+		("inf" "Infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1)
 		("ind" "induction #" holes-abbrev-complete 2)
 		("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
 		("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
@@ -191,7 +191,7 @@
       )
      ("Notations"
       "COMMAND               ABBREVIATION"
-      ["infix                           inf<C-BS>" (insert-and-expand "inf") t]     
+      ["Infix                           inf<C-BS>" (insert-and-expand "inf") t]     
       ["Notation (no assoc)             nota<C-BS>" (insert-and-expand "nota") t]     
       ["Notation (assoc)                notas<C-BS>" (insert-and-expand "notas") t]     
       ["Notation (no assoc, scope)      notasc<C-BS>" (insert-and-expand "notasc") t]     
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 39af0890..560d8aa3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -25,33 +25,35 @@
 (defvar coq-version-is-V6 nil 
 "This variable can be set to t to force ProofGeneral to coq version
 coq-6.x. To do that, put (setq coq-version-is-V6 t) in your .emacs and
-restart emacs. This variable overrides coq-version-is-V7 and
-coq-version-is-V74. If none of these 3 variables is set to t, then
-ProofGeneral guesses the version of coq by doing 'coqtop -v'.")
-
-(defvar coq-version-is-V7 nil
-  "This variable can be set to t to force ProofGeneral to coq version
-between coq-7.0 and coq-7.3.1. To do that, put (setq coq-version-is-V7 t) 
-in your .emacs and restart emacs. This variable overrides
-coq-version-is-V74 and is overrriden by coq-version-is-V6.  If none of
-these 3 variables is set to t, then ProofGeneral guesses the version of
-coq by doing 'coqtop -v'.")
-
-(defvar coq-version-is-V74 nil
-  "This variable can be set to t to force ProofGeneral to coq version
-coq-7.4. To do that, put (setq coq-version-is-V74 t) in your
-.emacs and restart emacs. This variable is overrriden by
-coq-version-is-V6 and coq-version-is-V7. If none of these 3 variables
-is set to t, then ProofGeneral guesses the version of coq by doing
-'coqtop -v'."  )
+restart emacs. This variable overrides coq-version-is-V7, V8 and
+V74. If none of these 3 variables is set to t, then ProofGeneral
+guesses the version of coq by doing 'coqtop -v'.")
+
+(defvar coq-version-is-V7 nil 
+"This variable can be set to t to force ProofGeneral to coq version
+between coq-7.0 and coq-7.3.1. To do that, put (setq coq-version-is-V7
+t) in your .emacs and restart emacs. This variable overrides
+coq-version-is-V74 and V8 and is overrriden by coq-version-is-V6.  If
+none of these 3 variables is set to t, then ProofGeneral guesses the
+version of coq by doing 'coqtop -v'.")
 
-(defvar coq-version-is-V8 nil
-  "This variable can be set to t to force ProofGeneral to coq version
+(defvar coq-version-is-V74 nil 
+"This variable can be set to t to force ProofGeneral to coq version
+coq-7.4. To do that, put (setq coq-version-is-V74 t) in your .emacs
+and restart emacs. This variable is overrriden by coq-version-is-V6
+and coq-version-is-V7. If none of these 3 variables is set to t, then
+ProofGeneral guesses the version of coq by doing 'coqtop -v'. If this
+variable is put to t (before PG is loaded) then V7 is automatically
+put to t."  )
+
+(defvar coq-version-is-V8 nil 
+"This variable can be set to t to force ProofGeneral to coq version
 above coq-8.0beta. To do that, put (setq coq-version-is-V8 t) in your
 .emacs and restart emacs. This variable is overrriden by
 coq-version-is-V6, coq-version-is-V7 and coq-version-is-V74. If none
 of these 4 variables is set to t, then ProofGeneral guesses the
-version of coq by doing 'coqtop -v'."  )
+version of coq by doing 'coqtop -v'. If this variable is put to t
+(before PG is loaded) then V74 is automatically put to t." )
 
 
 
diff --git a/coq/coq.el b/coq/coq.el
index 35c63e94..d64d4e93 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -622,7 +622,8 @@ Based on idea mentioned in Coq reference manual."
   (setq proof-terminal-char ?\.)
   (setq proof-script-command-end-regexp
         (if coq-version-is-V7 
-            "\\(?:\\w\\|\\s-\\|\\s)\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
+;            "\\(?:\\w\\|\\s-\\|\\s)\\|\\\\*\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)"
+            "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)"
           "[.]"))
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")