Custom Query (361 matches)

The manual mentions a 'Holes' feature in section §9.5. It seems that it activates as soon as the abbrev mode is loaded when opening a coq source file (.v), and appends its predefined abbreviations to the current abbrev table (if it already exists).

It is my understanding that this behavior forces quite a few abbreviations upon the user that fancies using emacs' abbrev-mode, without any way to deactivate this feature, short of editing the source code manually.

I'm using ProofGeneral to edit SSReflect Coq files (a syntaxic - among others - extension for Coq that makes the predefined abbreviations irrelevant), and would like to use the abbrev-mode without any modification of my abbrev-table.

Is there a way to deactivate the Holes feature that I have missed ?

OS: Mac OS X 10.5.4

PG version: 3.7.1

Gnu Emacs version: 22.2.1 (via MacPorts?), 23.0.60.1 (via CVS)

Coq version: 8.1pl3

Test file: A single line consisting of "Definition x : nat := 3."

Problem: Coq fails to start when I try to process the line or buffer. The only error message that I see is "Wrong type argument: integerp, "-emacs-U"." (For the CVS version of emacs, it's characterp instead of integerp.) In the *Messages* buffer, I see "let*: Wrong type argument: integerp, "-emacs-U" [2 times]." I don't think I'm seeing this problem with PG 3.7.

My contact: brian.aydemir [ at ] gmail.com

Cheers, Brian Aydemir

Setting save-abbrevs to nil in coq-install-abbrevs disables automatics saving of any abbreviation that the user defined in this emacs session. This is not acceptable for people who do use abbrevs.