From 65040f942717d5b8b5aaf3bf14bbfa76a128c832 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 15 Apr 2004 11:36:23 +0000
Subject: little change in CHANGES and in coq syntax table.

---
 CHANGES           | 8 ++++++++
 coq/coq-syntax.el | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index eb6d042e..a48209f5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -217,6 +217,14 @@ simple, holes are pieces of text that can be "filled" by different
 means. The new menu system makes use of the holes system. Almost all
 holes operations are available in the Coq/holes menu.
 
+Note: Holes and menus make use of emacs abbreviation mechanism, please
+make sure you don't have an abbrev table defined in you config files
+(C-h v abbrev-file-name to see the name of the abbreviation file). If
+there is already such a table, you can do the following to merge with
+ProofGeneral's abbrev: M-x read-abbrev-file, then find the file named
+"coq-abbrev.el" in the ProofGeneral/coq directory. At emacs exit you
+will be asked if you want to save abbrevs, answer yes.
+
 *** X-symbols are much improved (more symbols, cleaner grammar)
 
 Symbols are encoded only if between spaces or _'s. Sub/superscripts
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 6ff24e4d..d7684506 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -824,7 +824,7 @@ Idtac (Nop) tactic, put the following line in your .emacs:
   (modify-syntax-entry ?>  ".")
   (modify-syntax-entry ?\& ".")
   (modify-syntax-entry ?_  "w")
-  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\' "w")
   (modify-syntax-entry ?\| ".")
 
 ; should baybe be "_" but it makes coq-find-and-forget (in coq.el) bug
-- 
cgit v1.2.3