aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--acl2/acl2.el3
-rw-r--r--coq/coq.el2
2 files changed, 5 insertions, 0 deletions
diff --git a/acl2/acl2.el b/acl2/acl2.el
index 89808638..c45ca5ae 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -85,6 +85,9 @@
;; End of easy config.
)
+(eval-when-compile
+ (require 'proof-shell)) ; nuke warning
+
;; Interrupts and errors enter another loop; break out of it
(add-hook
'proof-shell-handle-error-or-interrupt-hook
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