Coq : deactivation of the 'Holes' functionality

[coquser]

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 ?

[David Aspinall]

I think we should allow the Holes feature to be turned off. To do this smoothly perhaps the holes symbols could be replaced by underscores in the insertion functions defined in coq.el which suppose holes are available.

But meanwhile, it looks as if the code intended not to trash your (local) abbrev table was faulty. I've patched it.

[courtieu]

The patch seems ok to me.

holes completion in abbreviations is now disabled if (customizable) variable coq-holes-minor-mode is set to nil.