aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-syntax.el
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <courtieu@lri.fr>2012-05-31 09:03:23 +0000
committerGravatar Pierre Courtieu <courtieu@lri.fr>2012-05-31 09:03:23 +0000
commit56f018fbcf5ee07eee3a0a463084446fef52415c (patch)
tree9d6b834566cea17f041e8ccf6e73aa471e819b63 /coq/coq-syntax.el
parentebaa1e401477bf892841ebb99701ed9d063547e6 (diff)
Fix of a bug. coq id can start with underscore.
Diffstat (limited to 'coq/coq-syntax.el')
-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 "\\)*"))