Make coq-load-path accept either strings (which are passed "-I" options)
or conses of strings (which are passed as "-R" options).


> (setq coq-load-path '(("~/coq/math-classes/src" . "MathClasses")
                        ("~/src/aac_tactics" . "AAC")))

> (coq-include-options nil)
("-R" "~/src/coq/math-classes/src" "MathClasses" "-I" "~/src/rippling" "-R" 
"~/src/aac_tactics" . "AAC")

Signed-off-by: Tom Prince <>
 ProofGeneral-4.1RC4/coq/coq.el |   31 +++++++++++++++++++------------
 1 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/ProofGeneral-4.1RC4/coq/coq.el b/ProofGeneral-4.1RC4/coq/coq.el
index b218f08..34d0529 100644
--- a/ProofGeneral-4.1RC4/coq/coq.el
+++ b/ProofGeneral-4.1RC4/coq/coq.el
@@ -1331,9 +1331,12 @@ contain \".\" for the current directory (see
 For coqdep and coqc these directories are passed via \"-I\"
-options over the command line. For interactive scripting an
-\"Add LoadPath\" command is used."
-  :type '(repeat string)
+or \"-R\" options over the command line. For interactive
+scripting an \"Add LoadPath\" command is used."
+  :type '(repeat (choice (string :tag "directory")
+                         (cons :tag "recursive directory"
+                                (string :tag "directory")
+                                (string :tag "coq path"))))
   :safe '(lambda (v) (every 'stringp v))
   :group 'coq-auto-compile)
@@ -1482,15 +1485,19 @@ arguments with `nconc'.
 FILE should be an absolute file name. It can be nil if
 `coq-load-path-include-current' is nil."
-  (let ((result nil))
-    (when coq-load-path
-      (setq result (list "-I" (expand-file-name (car coq-load-path))))
-      (dolist (dir (cdr coq-load-path))
-        (nconc result (list "-I" (expand-file-name dir)))))
-    (if coq-load-path-include-current
-        (setq result
-              (cons "-I" (cons (file-name-directory file) result))))
-    result))
+  (flet ((arg-from-option (arg)
+                          (if (consp arg)
+                              (list "-R" (expand-file-name (car arg)) (cdr 
+                            (list "-I" (expand-file-name arg)))))
+    (let ((result nil))
+      (when coq-load-path
+        (setq result (arg-from-option (car coq-load-path)))
+        (dolist (dir (cdr coq-load-path))
+          (nconc result (arg-from-option dir))))
+      (if coq-load-path-include-current
+          (setq result
+                (cons "-I" (cons (file-name-directory file) result))))
+      result)))
 (defun coq-init-compile-response-buffer (command)
   "Initialize the buffer for the compilation output.

ProofGeneral-devel mailing list

Reply via email to