aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 22:30:11 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2004-04-17 22:30:11 +0000
commit2968c81ed673a83ed338d9362324a591d1b1b792 (patch)
tree7eb27933a3a3d579d65a69cc4d25b945993dfb0e /coq
parentb642237b9e312e57743561e674d65c4b1f8f15ce (diff)
Compiler warnings
Diffstat (limited to 'coq')
-rw-r--r--coq/coq.el2
1 files changed, 2 insertions, 0 deletions
diff --git a/coq/coq.el b/coq/coq.el
index d664d2b3..001887ac 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -667,6 +667,8 @@ This is specific to coq-mode."
(message "%s%s.v" dir modname)
(format "%s%s.v" dir modname)))))
+ ;; FIXME da: coq-proof-shell-inform-file-retracted-cmd, etc, need
+ ;; defvars somewhere to avoid compiler warnings (or TBD: easy-config)
(setq coq-proof-shell-inform-file-retracted-cmd
;; da: This is a HORRIBLE fragile hack! Instead of issuing a
;; command to the prover we have to run a "coqdep" command to