aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2012-05-31 09:03:23 +0000
committerPierre Courtieu2012-05-31 09:03:23 +0000
commit56f018fbcf5ee07eee3a0a463084446fef52415c (patch)
tree9d6b834566cea17f041e8ccf6e73aa471e819b63
parentebaa1e401477bf892841ebb99701ed9d063547e6 (diff)
Fix of a bug. coq id can start with underscore.
-rw-r--r--coq/coq-syntax.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 27e4668e..ff62785d 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -901,7 +901,7 @@ It is used:
"A regexp indicating that the Coq process has identified an error.")
(defvar coq-id proof-id)
-(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)")
+(defvar coq-id-shy "\\(?:\\w\\|\\s_\\)+")
; do not use proof-ids with a space separator!
(defvar coq-ids (concat proof-id "\\(" "\\s-+" proof-id "\\)*"))