aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-03 08:52:26 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-10-03 08:52:26 +0000
commit5bce36660b3db1b7253278903376efa3cb938019 (patch)
tree6a328dc5ae5af7f5e540c86a46ec665095925e4f /coq
parent75a9e6fa64913e49e55557a6db1b50e8dbc7d25f (diff)
Move a comment to docstring
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 02af6c05..f3f0b230 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -108,14 +108,13 @@ Set to t if you want this feature."
:type 'string
:group 'coq)
-;; Command to initialize the Coq Proof Assistant
-
(defcustom coq-default-undo-limit 200
"Maximum number of Undo's possible when doing a proof."
:type 'number
:group 'coq)
(defconst coq-shell-init-cmd
+ "Command to initialize the Coq Proof Assistant."
(format "Set Undo %s . " coq-default-undo-limit))
(require 'coq-syntax)
@@ -1141,6 +1140,7 @@ This is specific to `coq-mode'."
;; FIXME: to handle "printing all" properly, we should change the state
;; of the variables that also depend on it.
+;; da:
(defpacustom print-fully-explicit nil
"Print fully explicit terms."
:type 'boolean