diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-07-05 17:53:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-07-05 17:53:29 +0000 |
| commit | 2438d15236e2e8264fdb2f6b91f4744d22492992 (patch) | |
| tree | d480e00e178ef9c2b0711b94172bf7fb90611aca /generic/pg-custom.el | |
| parent | 362e64643112d7a3179f1225e11511dfc8bd80e9 (diff) | |
Add use-holes setting.
Diffstat (limited to 'generic/pg-custom.el')
| -rw-r--r-- | generic/pg-custom.el | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/generic/pg-custom.el b/generic/pg-custom.el index 64d8a97a..3c74c3fb 100644 --- a/generic/pg-custom.el +++ b/generic/pg-custom.el @@ -190,6 +190,16 @@ http://proofgeneral.inf.ed.ac.uk/trac" :type 'file :group 'prover-config) +;; TODO: not used yet. Want to move specific enabling of holes modes +;; to generic code (coq.el enables it in script and shell). +;; See http://proofgeneral.inf.ed.ac.uk/trac/ticket/211 +(defpgcustom use-holes (eq proof-assistant-symbol 'coq) + "Whether or not to use the holes (editing template) mechanism. +Enabled by default for Coq." + :type 'boolean + :group 'prover-config) + + (provide 'pg-custom) |