diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 2 |
2 files changed, 9 insertions, 1 deletions
@@ -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 |