Custom Query (361 matches)

When using "Extraction Library <Module>", the "Library" word is not highlighted in blue like all other keywords (Extraction, Require, etc).

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 ?

The issue is that after changing the active scripting buffer, the first assert operation is lost, because the prover is not running. To reproduce go to coq/ex/test-cases/multiple-files-single-dir and do some scripting in, say, a.v. Then change to a different file (eg b.v) and do some scripting there. To clearly see the effect, make sure the second file (b.v) does not start with a comment.

There is a patch in ​http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000114.html but it needs reviewing.