aboutsummaryrefslogtreecommitdiff
path: root/coq
diff options
context:
space:
mode:
authorDavid Aspinall2009-08-19 16:36:49 +0000
committerDavid Aspinall2009-08-19 16:36:49 +0000
commit32110e70622b2db165b4a514a935197f00ebbd3e (patch)
treeedf6aa75ca7f4945413cc4425d2bc70d93af97f9 /coq
parent5c938d2d0e2d1ed153f5672c9e2eb1da8d5b930a (diff)
*** empty log message ***
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el11
1 files changed, 11 insertions, 0 deletions
diff --git a/coq/coq.el b/coq/coq.el
index e38c215f..5d2cab81 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -823,6 +823,17 @@ This is specific to `coq-mode'."
(if coq-version-is-V8-1 "-emacs-U" "-emacs")))
coq-prog-name))))
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Holes mode switch
+
+;; TODO: complete and maybe make this generic (with prover-specific default?
+;; or use same mechanism as tokens, etc?)
+(defpacustom use-editing-holes nil
+ "Enable holes for editing."
+ :type 'boolean)
+;; :eval (set-stuff-for-holes)
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Configuring proof and pbp mode and setting up various utilities ;;