aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1999-02-03 15:55:42 +0000
committerGravatar Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>1999-02-03 15:55:42 +0000
commit113a83d751f3fc51fc6fc6655e3ee77f488b2793 (patch)
tree1ef34cc2d8dc80237684c187d381cbc29fb6d334 /coq
parentc28be95727fe2023d2937958ac53aa1716958337 (diff)
fixed syntax entry for "_"
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el5
1 files changed, 1 insertions, 4 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 7eaf7f51..160ec044 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -309,10 +309,7 @@
(setq proof-mode-for-pbp 'coq-pbp-mode)
)
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Configuring proof and pbp mode and setting up various utilities ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
+; FIXME: IMHO (tms) this ought to be defined in coq-syntax and not here.
(defun coq-init-syntax-table ()
"Set appropriate values for syntax table in current buffer."