aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-seq-compile.el
diff options
context:
space:
mode:
authorGravatar Hendrik Tews <hendrik@askra.de>2016-11-16 11:27:42 +0100
committerGravatar Hendrik Tews <hendrik@askra.de>2016-11-16 11:41:51 +0100
commit94e8ce4389c1d9926a629d30075dae64bee84779 (patch)
treeb8d59815aafaf817d7f4025ee5d20c3c0e94d6ad /coq/coq-seq-compile.el
parentc1e06d2c2d67236aeedb59137d155d93d0646596 (diff)
first version for quick compilation
Select "Quick compilation mode" in the Coq menu. See also documentation of coq-compile-quick, the and-vio2vo stuff is not yet there.
Diffstat (limited to 'coq/coq-seq-compile.el')
-rw-r--r--coq/coq-seq-compile.el6
1 files changed, 3 insertions, 3 deletions
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index da85ad9f..031fc492 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -212,7 +212,7 @@ function."
(setq result '(0 0))
(let* ((lib-src-file
(expand-file-name
- (coq-library-src-of-obj-file lib-obj-file)))
+ (coq-library-src-of-vo-file lib-obj-file)))
dependencies deps-mod-time)
(if (file-exists-p lib-src-file)
;; recurse into dependencies now
@@ -260,7 +260,7 @@ therefore the customizations for `compile' do not apply."
(let* ((local-compile-command coq-compile-command)
(physical-dir (file-name-directory absolute-module-obj-file))
(module-object (file-name-nondirectory absolute-module-obj-file))
- (module-source (coq-library-src-of-obj-file module-object))
+ (module-source (coq-library-src-of-vo-file module-object))
(requiring-file buffer-file-name))
(mapc
(lambda (substitution)
@@ -282,7 +282,7 @@ therefore the customizations for `compile' do not apply."
(compilation-start local-compile-command)
(coq-seq-lock-ancestor
span
- (coq-library-src-of-obj-file absolute-module-obj-file)))))
+ (coq-library-src-of-vo-file absolute-module-obj-file)))))
(defun coq-seq-map-module-id-to-obj-file (module-id span &optional from)
"Map MODULE-ID to the appropriate coq object file.