use coq-- for internal compilation variables

1 files changed, 139 insertions, 139 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 00ddedbc..6dbfb109 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -102,7 +102,7 @@
 ;;
 ;; The problem is solved with the 'coq-locked-ancestors property of
 ;; spans that contain Require commands and with the
-;; coq-par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors
+;; coq--par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors
 ;; property are unlocked when this span is retracted. As locking is
 ;; done eagerly (as soon as coqdep runs first on the file), I only
 ;; have to make sure the right files appear in 'coq-locked-ancestors.
@@ -111,7 +111,7 @@
 ;; walks upwards the dependency tree. In the end, every top-level job
 ;; contains a list of all its direct and indirect ancestors. Because
 ;; of eager locking, all its ancestors are already locked, when a
-;; top-level job is about to be retired. The coq-par-ancestor-files
+;; top-level job is about to be retired. The coq--par-ancestor-files
 ;; hash therefore records whether some ancestor does already appear in
 ;; the 'coq-locked-ancestors property of some span before the current
 ;; one. If it doesn't, I store it in the current span.
@@ -244,7 +244,7 @@
 ;;                                the process is killed
 ;;
 ;;
-;; Symbols in the coq-par-ancestor-files hash
+;; Symbols in the coq--par-ancestor-files hash
 ;;
 ;; This hash maps file names to symbols. A file is present in the
 ;; hash, if it has been locked.
@@ -269,7 +269,7 @@
 ;; 	     (mapc (lambda (p) (when (eq (get p 'type) 'clone)
 ;; 				 (push p clones)))
 ;; 		   (get v 'coqc-dependants)))
-;; 	   coq-compilation-object-hash)
+;; 	   coq--compilation-object-hash)
 ;;   (mapc (lambda (v)
 ;; 	  (message "%s type %s for %s state %s dep of %s queue dep of %s"
 ;; 		   (get v 'name)
@@ -283,7 +283,7 @@
 
 ;;; Variables
 
-(defvar coq-par-ancestor-files nil
+(defvar coq--par-ancestor-files nil
   "Hash remembering the state of locked ancestor files.
 This hash maps true file names (in the sense of `file-truename')
 to either 'locked or 'asserted.
@@ -299,10 +299,10 @@ asserted region.
 asserted required module (and is in some 'coq-locked-ancestors
 property).")
 
-(defvar coq-current-background-jobs 0
+(defvar coq--current-background-jobs 0
   "Number of currently running background jobs.")
 
-(defvar coq-compilation-object-hash nil
+(defvar coq--compilation-object-hash nil
   "Hash for storing the compilation jobs.
 This hash only stores real compilation jobs and no clones. They
 are stored in order to avoid double compilation. The jobs stored
@@ -311,17 +311,17 @@ information in their property list. See the documentation in the
 source file \"coq-par-compile.el\". The hash always maps .vo file
 names to compilation jobs, regardless of ``-quick''.")
 
-(defvar coq-last-compilation-job nil
+(defvar coq--last-compilation-job nil
   "Pointer to the last top-level compilation job.
 Used to link top-level jobs with queue dependencies.")
 
-(defvar coq-compile-vio2vo-in-progress nil
+(defvar coq--compile-vio2vo-in-progress nil
   "Set to t iff vio2vo is running in background.")
 
-(defvar coq-compile-vio2vo-delay-timer nil
+(defvar coq--compile-vio2vo-delay-timer nil
   "Holds the timer for the vio2vo delay.")
 
-(defvar coq-par-next-id 1
+(defvar coq--par-next-id 1
   "Increased for every job and process, to get unique job names.
 The names are only used for debugging.")
 
@@ -363,15 +363,15 @@ latter greater then everything else."
    (t (time-less-p time-1 time-2))))
 
 (defun coq-par-init-compilation-hash ()
-  "(Re-)Initialize `coq-compilation-object-hash'."
-  (setq coq-compilation-object-hash (make-hash-table :test 'equal)))
+  "(Re-)Initialize `coq--compilation-object-hash'."
+  (setq coq--compilation-object-hash (make-hash-table :test 'equal)))
 
 (defun coq-par-init-ancestor-hash ()
-  "(Re-)Initialize `coq-par-ancestor-files'"
-  (setq coq-par-ancestor-files (make-hash-table :test 'equal))
+  "(Re-)Initialize `coq--par-ancestor-files'"
+  (setq coq--par-ancestor-files (make-hash-table :test 'equal))
   (mapc
    (lambda (locked-anc)
-     (puthash locked-anc 'asserted coq-par-ancestor-files))
+     (puthash locked-anc 'asserted coq--par-ancestor-files))
    proof-included-files-list))
 
 ;;; generic queues
@@ -405,13 +405,13 @@ queue.")
 (defun coq-par-job-enqueue (job)
   "Insert job in the queue of waiting compilation jobs."
   (coq-par-enqueue coq-par-compilation-queue job)
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "%s: enqueue job in waiting queue" (get job 'name))))
 
 (defun coq-par-job-dequeue ()
   "Dequeue the next job from the compilation queue."
   (let ((res (coq-par-dequeue coq-par-compilation-queue)))
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(if res
 	    (message "%s: dequeue" (get res 'name))
 	  (message "compilation queue empty")))
@@ -428,13 +428,13 @@ access the queue.")
 (defun coq-par-vio2vo-enqueue (job)
   "Insert JOB in the queue for vio2vo processing."
   (coq-par-enqueue coq-par-vio2vo-queue job)
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "%s: enqueue job in vio2vo queue" (get job 'name))))
 
 (defun coq-par-vio2vo-dequeue ()
   "Dequeue the next job from the vio2vo queue."
   (let ((res (coq-par-dequeue coq-par-vio2vo-queue)))
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(if res
 	    (message "%s: vio2vo dequeue" (get res 'name))
 	  (message "vio2vo queue empty")))
@@ -530,13 +530,13 @@ If no circle is found return nil, otherwise the list of files
 belonging to the circle."
   (let (cycle result)
     (maphash (lambda (key job) (put job 'visited nil))
-	     coq-compilation-object-hash)
+	     coq--compilation-object-hash)
     (maphash
      (lambda (key job)
        (when (and (not cycle) (not (get job 'visited))
 		  (eq (get job 'state) 'waiting-dep))
 	 (setq cycle (coq-par-find-dependency-circle-for-job job nil))))
-     coq-compilation-object-hash)
+     coq--compilation-object-hash)
     (dolist (j cycle)
       (when (eq (get j 'type) 'file)
 	(push (get j 'src-file) result)))
@@ -570,7 +570,7 @@ this buffer visible and returns a string.
 This function does always return .vo dependencies, regardless of the
 value of `coq-compile-quick'. If necessary, the conversion into .vio
 files must be done elsewhere."
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "analyse coqdep output \"%s\"" output))
   (if (or
        (not (eq status 0))
@@ -625,10 +625,10 @@ depending on `coq-compile-quick', must be done elsewhere."
 			   (cons command-intro this-command)
 			 this-command))
 	 coqdep-status coqdep-output)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "Run synchronously: %s"
 		 (mapconcat 'identity full-command " ")))
-    ;; (if coq-debug-auto-compilation
+    ;; (if coq--debug-auto-compilation
     ;;     (message "CPGLD: call coqdep arg list: %s" coqdep-arguments))
     (with-temp-buffer
       (setq coqdep-status
@@ -636,7 +636,7 @@ depending on `coq-compile-quick', must be done elsewhere."
                    coq-dependency-analyzer nil (current-buffer) nil
                    coqdep-arguments))
       (setq coqdep-output (buffer-string)))
-    ;; (if coq-debug-auto-compilation
+    ;; (if coq--debug-auto-compilation
     ;;     (message "CPGLD: coqdep status %s, output on %s: %s"
     ;;              coqdep-status lib-src-file coqdep-output))
     (coq-par-analyse-coq-dep-exit coqdep-status coqdep-output full-command)))
@@ -676,7 +676,7 @@ function returns () if MODULE-ID comes from the standard library."
 		 coq-load-path
                  (concat "echo \"" coq-string "\" > " temp-require-file ";"))))
       (delete-file temp-require-file))
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "coq-par-get-library-dependencies delivered \"%s\"" result))
     (if (stringp result)
         ;; Error handling: coq-par-get-library-dependencies was not able to
@@ -726,38 +726,38 @@ function returns () if MODULE-ID comes from the standard library."
        (when (process-get process 'coq-compilation-job)
 	 (process-put process 'coq-par-process-killed t)
 	 (delete-process process)
-	 (when coq-debug-auto-compilation
+	 (when coq--debug-auto-compilation
 	   (message "%s %s: kill it"
 		    (get (process-get process 'coq-compilation-job) 'name)
 		    (process-name process)))))
      (process-list))
-    (setq coq-current-background-jobs 0)))
+    (setq coq--current-background-jobs 0)))
 
 (defun coq-par-unlock-ancestors-on-error ()
   "Unlock ancestors which are not in an asserted span.
 Used for unlocking ancestors on compilation errors."
-  (when coq-par-ancestor-files
+  (when coq--par-ancestor-files
     ;; nil e.g. when enabling on-the-fly compilation after processing imports.
     (maphash
      (lambda (ancestor state)
        (when (eq state 'locked)
          (coq-unlock-ancestor ancestor)
-         (puthash ancestor nil coq-par-ancestor-files)))
-     coq-par-ancestor-files)))
+         (puthash ancestor nil coq--par-ancestor-files)))
+     coq--par-ancestor-files)))
 
 (defun coq-par-emergency-cleanup ()
   "Emergency cleanup for parallel background compilation.
 Kills all processes, unlocks ancestors, clears the queue region
 and resets the internal state."
-  (when coq-debug-auto-compilation
+  (when coq--debug-auto-compilation
     (message "emergency cleanup"))
   (coq-par-kill-all-processes)
   (setq coq-par-compilation-queue (coq-par-new-queue))
-  (setq coq-last-compilation-job nil)
+  (setq coq--last-compilation-job nil)
   (setq coq-par-vio2vo-queue (coq-par-new-queue))
-  (setq coq-compile-vio2vo-in-progress nil)
-  (when coq-compile-vio2vo-delay-timer
-    (cancel-timer coq-compile-vio2vo-delay-timer))
+  (setq coq--compile-vio2vo-in-progress nil)
+  (when coq--compile-vio2vo-delay-timer
+    (cancel-timer coq--compile-vio2vo-delay-timer))
   (when proof-action-list
     (setq proof-shell-interrupt-pending t))
   (coq-par-unlock-ancestors-on-error)
@@ -778,10 +778,10 @@ compilation job JOB, making sure that CONTINUATION runs when the
 process finishes successfully. FILE-RM, if not nil, denotes a
 file to be deleted when the process is killed."
   (let ((process-connection-type nil)	; use pipes
-	(process-name (format "pro-%s" coq-par-next-id))
+	(process-name (format "pro-%s" coq--par-next-id))
 	process)
     (with-current-buffer (or proof-script-buffer (current-buffer))
-      (if coq-debug-auto-compilation
+      (if coq--debug-auto-compilation
 	  (message "%s %s: start %s %s in %s"
 		   (get job 'name) process-name
 		   command (mapconcat 'identity arguments " ")
@@ -800,8 +800,8 @@ file to be deleted when the process is killed."
       (set-process-filter process 'coq-par-process-filter)
       (set-process-sentinel process 'coq-par-process-sentinel)
       (set-process-query-on-exit-flag process nil)
-      (setq coq-par-next-id (1+ coq-par-next-id))
-      (setq coq-current-background-jobs (1+ coq-current-background-jobs))
+      (setq coq--par-next-id (1+ coq--par-next-id))
+      (setq coq--current-background-jobs (1+ coq--current-background-jobs))
       (process-put process 'coq-compilation-job job)
       (process-put process 'coq-process-continuation continuation)
       (process-put process 'coq-process-command (cons command arguments))
@@ -817,7 +817,7 @@ errors are reported with an error message."
   (condition-case err
       (if (process-get process 'coq-par-process-killed)
 	  (progn
-	    (if coq-debug-auto-compilation
+	    (if coq--debug-auto-compilation
 		(message "%s %s: skip sentinel, process killed, %s"
 			 (get (process-get process 'coq-compilation-job) 'name)
 			 (process-name process)
@@ -830,13 +830,13 @@ errors are reported with an error message."
 		  (delete-file (process-get process 'coq-process-rm))))
 	    (when (eq (process-get process 'coq-process-continuation)
 		      'coq-par-vio2vo-continuation)
-	      (when coq-debug-auto-compilation
+	      (when coq--debug-auto-compilation
 		(message "%s: reenqueue for vio2vo"
 			 (get (process-get process 'coq-compilation-job) 'name)))
 	      (coq-par-vio2vo-enqueue
 	       (process-get process 'coq-compilation-job))))
 	(let (exit-status)
-	  (if coq-debug-auto-compilation
+	  (if coq--debug-auto-compilation
 	      (message "%s %s: process status changed to %s"
 		       (get (process-get process 'coq-compilation-job) 'name)
 		       (process-name process)
@@ -845,18 +845,18 @@ errors are reported with an error message."
 	   ((eq (process-status process) 'exit)
 	    (setq exit-status (process-exit-status process)))
 	   (t (setq exit-status "abnormal termination")))
-	  (setq coq-current-background-jobs
-		(max 0 (1- coq-current-background-jobs)))
+	  (setq coq--current-background-jobs
+		(max 0 (1- coq--current-background-jobs)))
 	  (funcall (process-get process 'coq-process-continuation)
 		   process exit-status)
 	  (coq-par-start-jobs-until-full)
-	  (when (and coq-compile-vio2vo-in-progress
-		     (eq coq-current-background-jobs 0))
-	    (setq coq-compile-vio2vo-in-progress nil)
+	  (when (and coq--compile-vio2vo-in-progress
+		     (eq coq--current-background-jobs 0))
+	    (setq coq--compile-vio2vo-in-progress nil)
 	    (message "vio2vo compilation finished"))
 	  (when (and
-		 (eq coq-current-background-jobs 0)
-		 coq-last-compilation-job)
+		 (eq coq--current-background-jobs 0)
+		 coq--last-compilation-job)
 	    (let ((cycle (coq-par-find-dependency-circle)))
 	      (if cycle
 		  (signal 'coq-compile-error-circular-dep
@@ -881,11 +881,11 @@ errors are reported with an error message."
 
 (defun coq-par-run-vio2vo-queue ()
   "Start delayed vio2vo compilation."
-  (assert (not coq-last-compilation-job)
+  (assert (not coq--last-compilation-job)
 	  nil "normal compilation and vio2vo in parallel 3")
-  (setq coq-compile-vio2vo-in-progress t)
-  (setq coq-compile-vio2vo-delay-timer nil)
-  (when coq-debug-auto-compilation
+  (setq coq--compile-vio2vo-in-progress t)
+  (setq coq--compile-vio2vo-delay-timer nil)
+  (when coq--debug-auto-compilation
     (message "Start vio2vo processing for %d jobs"
 	     (+ (length (car coq-par-vio2vo-queue))
 		(length (cdr coq-par-vio2vo-queue)))))
@@ -896,9 +896,9 @@ errors are reported with an error message."
 This callback is inserted with a dummy item after the last
 require command to start vio2vo compilation after
 `coq-compile-vio2vo-delay' seconds."
-  (assert (not coq-last-compilation-job)
+  (assert (not coq--last-compilation-job)
 	  nil "normal compilation and vio2vo in parallel 1")
-  (setq coq-compile-vio2vo-delay-timer
+  (setq coq--compile-vio2vo-delay-timer
 	(run-at-time coq-compile-vio2vo-delay nil 'coq-par-run-vio2vo-queue)))
 
 
@@ -922,7 +922,7 @@ require command to start vio2vo compilation after
   (put dependant 'coqc-dependency-count
        (1+ (get dependant 'coqc-dependency-count)))
   (push dependant (get dependee 'coqc-dependants))
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "%s -> %s: add coqc dependency"
 	       (get dependee 'name) (get dependant 'name))))
 
@@ -933,7 +933,7 @@ require command to start vio2vo compilation after
 	  nil "queue dependency cannot be added")
   (put dependant 'queue-dependant-waiting t)
   (put dependee 'queue-dependant dependant)
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "%s -> %s: add queue dependency"
 	       (get dependee 'name) (get dependant 'name))))
 
@@ -961,7 +961,7 @@ therefore delete a file if it might be in the way. Sets the
 	 (src-time (nth 5 (file-attributes (get job 'src-file))))
 	 file-to-delete max-obj-time vio-is-newer
 	 other-file other-obj-time result)
-    (when coq-debug-auto-compilation
+    (when coq--debug-auto-compilation
       (message
        (concat "%s: compare mod times: vo mod %s, vio mod %s, src mod %s, "
 	       "youngest dep %s; vo < src : %s, vio < src : %s, "
@@ -1012,7 +1012,7 @@ therefore delete a file if it might be in the way. Sets the
 	    (put job 'required-obj-file vo-file)
 	    (when vio-obj-time
 	      (setq file-to-delete vio-file)))
-	  (when coq-debug-auto-compilation
+	  (when coq--debug-auto-compilation
 	    (message
 	     (concat "%s: definitely need to compile to %s; delete %s")
 	     (get job 'name)
@@ -1038,7 +1038,7 @@ therefore delete a file if it might be in the way. Sets the
 				 (time-less-or-equal vio-obj-time src-time)
 				 (time-less-or-equal vio-obj-time dep-time)))
 		    (setq file-to-delete vio-file))
-		  (when coq-debug-auto-compilation
+		  (when coq--debug-auto-compilation
 		    (message "%s: vo up-to-date 1; delete %s"
 			     (get job 'name)
 			     (if file-to-delete file-to-delete "noting"))))
@@ -1049,7 +1049,7 @@ therefore delete a file if it might be in the way. Sets the
 			 (or (time-less-or-equal vio-obj-time src-time)
 			     (time-less-or-equal vio-obj-time dep-time)))
 		(setq file-to-delete vio-file))
-	      (when coq-debug-auto-compilation
+	      (when coq--debug-auto-compilation
 		(message "%s: need to compile to vo; delete %s"
 			 (get job 'name)
 			 (if file-to-delete file-to-delete "noting")))))
@@ -1073,7 +1073,7 @@ therefore delete a file if it might be in the way. Sets the
 	    (progn
 	      (put job 'required-obj-file other-file)
 	      (put job 'obj-mod-time other-obj-time)
-	      (when coq-debug-auto-compilation
+	      (when coq--debug-auto-compilation
 		(message (concat "%s: .vio and .vo up-to-date, "
 				 "continue with the older %s")
 			 (get job 'name)
@@ -1088,13 +1088,13 @@ therefore delete a file if it might be in the way. Sets the
 		(put job 'obj-mod-time vio-obj-time)
 		(when (eq coq-compile-quick 'quick-and-vio2vo)
 		  (put job 'vio2vo-needed t))
-		(when coq-debug-auto-compilation
+		(when coq--debug-auto-compilation
 		  (message "%s: vio up-to-date; delete %s"
 			   (get job 'name)
 			   (if file-to-delete file-to-delete "noting"))))
 	    (put job 'required-obj-file vo-file)
 	    (put job 'obj-mod-time vo-obj-time)
-	    (when coq-debug-auto-compilation
+	    (when coq--debug-auto-compilation
 	      (message "%s: vo up-to-date 2; delete %s"
 		       (get job 'name)
 		       (if file-to-delete file-to-delete "noting")))))))
@@ -1111,37 +1111,37 @@ This transition is only possible if JOB is in state
 'waiting-queue and if it has no queue dependee. If this is the
 case, the following actions are taken:
 - for top-level jobs (non-nil 'require-span property), ancestors
-  are registered in `coq-par-ancestor-files' and in the span in
+  are registered in `coq--par-ancestor-files' and in the span in
   'queue-span
 - processing of items in 'queueitems is started
 - a possible queue dependant gets it's dependency cleared, and,
   if possible the 'waiting-queue -> 'ready transition
   is (recursively) done for the dependant
 - if this job is the last top-level compilation
-  job (`coq-last-compilation-job') then the last compilation job
+  job (`coq--last-compilation-job') then the last compilation job
   and `proof-second-action-list-active' are cleared."
   (if (or (not (eq (get job 'state) 'waiting-queue))
 	  (get job 'queue-dependant-waiting))
-      (if coq-debug-auto-compilation
+      (if coq--debug-auto-compilation
 	  (if (not (eq (get job 'state) 'waiting-queue))
 	      (message "%s: no queue kickoff because in state %s"
 		       (get job 'name) (get job 'state))
 	    (message
 	     "%s: no queue kickoff because waiting for queue dependency"
 	     (get job 'name))))
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "%s: has itself no queue dependency" (get job 'name)))
     (when (and (get job 'require-span) coq-lock-ancestors)
       (let ((span (get job 'require-span)))
 	(dolist (f (get job 'ancestor-files))
-	  (unless (eq (gethash f coq-par-ancestor-files) 'asserted)
-	    (puthash f 'asserted coq-par-ancestor-files)
+	  (unless (eq (gethash f coq--par-ancestor-files) 'asserted)
+	    (puthash f 'asserted coq--par-ancestor-files)
 	    (span-set-property
 	     span 'coq-locked-ancestors
 	     (cons f (span-property span 'coq-locked-ancestors)))))))
     (when (get job 'queueitems)
       (let ((items (get job 'queueitems)))
-	(when (and (eq coq-last-compilation-job job)
+	(when (and (eq coq--last-compilation-job job)
 		   (eq coq-compile-quick 'quick-and-vio2vo))
 	  ;; Insert the vio2vo start notification callback after the
 	  ;; require item.
@@ -1157,34 +1157,34 @@ case, the following actions are taken:
 		  (list nil nil 'coq-par-require-processed)
 		  (cdr items)))))
 	(proof-add-to-queue items 'advancing)
-	(if coq-debug-auto-compilation
+	(if coq--debug-auto-compilation
 	    (message "%s: add %s items to action list"
 		     (get job 'name) (length items)))
 	(put job 'queueitems nil)))
     (put job 'state 'ready)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "%s: ready" (get job 'name)))
     (let ((dependant (get job 'queue-dependant)))
       (if dependant
 	  (progn
-	    (assert (not (eq coq-last-compilation-job job))
-		    nil "coq-last-compilation-job invariant error")
+	    (assert (not (eq coq--last-compilation-job job))
+		    nil "coq--last-compilation-job invariant error")
 	    (put dependant 'queue-dependant-waiting nil)
-	    (if coq-debug-auto-compilation
+	    (if coq--debug-auto-compilation
 		(message
 		 "%s -> %s: clear queue dependency, kickoff queue at %s"
 		 (get job 'name) (get dependant 'name) (get dependant 'name)))
 	    (coq-par-kickoff-queue-maybe dependant)
-	    (if coq-debug-auto-compilation
+	    (if coq--debug-auto-compilation
 		(message "%s: queue kickoff finished"
 			 (get job 'name))))
-	(when (eq coq-last-compilation-job job)
-	  (setq coq-last-compilation-job nil)
+	(when (eq coq--last-compilation-job job)
+	  (setq coq--last-compilation-job nil)
 	  (setq proof-second-action-list-active nil)
-	  (if coq-debug-auto-compilation
+	  (if coq--debug-auto-compilation
 	      (message "clear last compilation job"))
 	  (message "Library compilation finished"))
-	(if coq-debug-auto-compilation
+	(if coq--debug-auto-compilation
 	    (message "%s: no queue dependant, queue kickoff finished"
 		     (get job 'name)))))))
 
@@ -1204,7 +1204,7 @@ possible, also 'waiting-queue -> 'ready."
   ;; It also puts job into the vio2vo queue, if necessary.
   (if (coq-par-job-needs-compilation job)
       (coq-par-start-or-enqueue job)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "%s: up-to-date, no compilation" (get job 'name)))
     (when (get job 'vio2vo-needed)
       (coq-par-vio2vo-enqueue job))
@@ -1235,7 +1235,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
        (1- (get dependant 'coqc-dependency-count)))
   (assert (<= 0 (get dependant 'coqc-dependency-count))
 	  nil "dependency count below zero")
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (message "%s: coqc dependency count down to %d"
 	       (get dependant 'name) (get dependant 'coqc-dependency-count)))
   (when (coq-par-dependencies-ready dependant)
@@ -1279,7 +1279,7 @@ This function makes the following actions.
     (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone))
       (setq dep-time (get job 'obj-mod-time)))
     (put job 'youngest-coqc-dependency dep-time)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "%s: kickoff %d coqc dependencies with time %s"
 		 (get job 'name) (length (get job 'coqc-dependants))
 		 (if (eq dep-time 'just-compiled)
@@ -1290,7 +1290,7 @@ This function makes the following actions.
      (lambda (dependant)
        (coq-par-decrease-coqc-dependency dependant dep-time ancestor-files))
      (get job 'coqc-dependants))
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "%s: coqc kickoff finished, maybe kickoff queue"
 		 (get job 'name)))
     (coq-par-kickoff-queue-maybe job)))
@@ -1299,13 +1299,13 @@ This function makes the following actions.
   "Start coqdep for JOB.
 Besides starting the background process, the source file is
 locked, registered in the 'ancestor-files property of JOB and in
-`coq-par-ancestor-files'"
+`coq--par-ancestor-files'"
   (let ((true-src (file-truename (get job 'src-file))))
     (when coq-lock-ancestors
       (proof-register-possibly-new-processed-file true-src)
       (put job 'ancestor-files (list true-src))
-      (unless (gethash true-src coq-par-ancestor-files)
-	(puthash true-src 'locked coq-par-ancestor-files)))
+      (unless (gethash true-src coq--par-ancestor-files)
+	(puthash true-src 'locked coq--par-ancestor-files)))
     (coq-par-start-process
      coq-dependency-analyzer
      (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path))
@@ -1319,7 +1319,7 @@ locked, registered in the 'ancestor-files property of JOB and in
 	(module (coq-module-of-src-file (get job 'src-file)))
 	(default-directory
 	  (file-name-directory (file-truename (get job 'src-file)))))
-    (when coq-debug-auto-compilation
+    (when coq--debug-auto-compilation
       (message "%s: start vio2vo for %s"
 	       (get job 'name)
 	       (get job 'src-file)))
@@ -1359,12 +1359,12 @@ coqdep or coqc are started for it."
 
 (defun coq-par-start-jobs-until-full ()
   "Start background jobs until the limit is reached."
-  (let ((max-jobs (if coq-compile-vio2vo-in-progress
+  (let ((max-jobs (if coq--compile-vio2vo-in-progress
 		      coq--internal-max-vio2vo-jobs
 		    coq--internal-max-jobs))
 	next-job)
-    (while (and (< coq-current-background-jobs max-jobs)
-		(setq next-job (if coq-compile-vio2vo-in-progress
+    (while (and (< coq--current-background-jobs max-jobs)
+		(setq next-job (if coq--compile-vio2vo-in-progress
 				   (coq-par-vio2vo-dequeue)
 				 (coq-par-job-dequeue))))
       (coq-par-start-task next-job))))
@@ -1374,7 +1374,7 @@ coqdep or coqc are started for it."
 NEW-JOB goes already into the waiting queue, if the number of
 background jobs is one below the limit. This is in order to leave
 room for Proof General."
-  (if (< (1+ coq-current-background-jobs) coq--internal-max-jobs)
+  (if (< (1+ coq--current-background-jobs) coq--internal-max-jobs)
       (coq-par-start-task new-job)
     (coq-par-job-enqueue new-job)))
 
@@ -1407,10 +1407,10 @@ there is space, coqdep is started immediately, otherwise the new
 job is put into the compilation queue.
 
 This function returns the newly created job."
-  (let* ((orig-job (gethash module-vo-file coq-compilation-object-hash))
+  (let* ((orig-job (gethash module-vo-file coq--compilation-object-hash))
 	 (new-job (make-symbol "coq-compile-job-symbol")))
-    (put new-job 'name (format "job-%d" coq-par-next-id))
-    (setq coq-par-next-id (1+ coq-par-next-id))
+    (put new-job 'name (format "job-%d" coq--par-next-id))
+    (setq coq--par-next-id (1+ coq--par-next-id))
     (put new-job 'vo-file module-vo-file)
     (put new-job 'coqc-dependency-count 0)
     (put new-job 'require-span require-span)
@@ -1419,7 +1419,7 @@ This function returns the newly created job."
 	;; there is already a compilation job for module-vo-file
 	(progn
 	  (put new-job 'type 'clone)
-	  (if coq-debug-auto-compilation
+	  (if coq--debug-auto-compilation
 	      (message "%s: create %s compilation job for %s"
 		       (get new-job 'name) (get new-job 'type) module-vo-file))
 	  (when queue-dep
@@ -1446,8 +1446,8 @@ This function returns the newly created job."
       (message "Check %s" (get new-job 'src-file))
       (put new-job 'load-path coq-load-path)
       (put new-job 'youngest-coqc-dependency '(0 0))
-      (puthash module-vo-file new-job coq-compilation-object-hash)
-      (if coq-debug-auto-compilation
+      (puthash module-vo-file new-job coq--compilation-object-hash)
+      (if coq--debug-auto-compilation
 	  (message "%s: create %s compilation for %s"
 		   (get new-job 'name) (get new-job 'type) module-vo-file))
       (when queue-dep
@@ -1485,7 +1485,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
 	(signal 'coq-compile-error-coqdep (get job 'src-file))
 
       ;; no coqdep error -- work on dependencies
-      (if coq-debug-auto-compilation
+      (if coq--debug-auto-compilation
 	  (message "%s: dependencies of %s are %s"
 		   (get job 'name) (get job 'src-file) dependencies-or-error))
       (put job 'state 'waiting-dep)
@@ -1506,10 +1506,10 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
       (put job 'youngest-coqc-dependency job-max-time)
       (if (coq-par-dependencies-ready job)
 	  (progn
-	    (if coq-debug-auto-compilation
+	    (if coq--debug-auto-compilation
 		(message "%s: coqc dependencies finished" (get job 'name)))
 	    (coq-par-compile-job-maybe job))
-	(if coq-debug-auto-compilation
+	(if coq--debug-auto-compilation
 	    (message "%s: wait for %d dependencies"
 		     (get job 'name) (get job 'coqc-dependency-count)))))))
 
@@ -1537,9 +1537,9 @@ PROCESS."
   (let ((job (process-get process 'coq-compilation-job)))
     (if (eq exit-status 0)
 	;; success - nothing to do
-	(when coq-debug-auto-compilation
+	(when coq--debug-auto-compilation
 	  (message "%s: vio2vo finished successfully" (get job 'name)))
-      (when coq-debug-auto-compilation
+      (when coq--debug-auto-compilation
 	(message "%s: vio2vo failed" (get job 'name)))
       (coq-compile-display-error
        (concat
@@ -1560,12 +1560,12 @@ PROCESS."
 This function translates MODULE-ID to a file name. If compilation
 for this file is not ignored, a new top-level compilation job is
 created. If there is a new top-level compilation job, it is saved
-in `coq-last-compilation-job'.
+in `coq--last-compilation-job'.
 
 This function must be evaluated with the buffer that triggered
 the compilation as current, otherwise a wrong `coq-load-path'
 might be used."
-  (if coq-debug-auto-compilation
+  (if coq--debug-auto-compilation
       (if from
 	  (message "handle required module \"%s\" from \"%s\"" module-id from)
 	(message "handle required module \"%s\" without from clause"
@@ -1573,7 +1573,7 @@ might be used."
   (let ((module-vo-file
 	 (coq-par-map-module-id-to-vo-file module-id coq-load-path from))
 	module-job)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(if module-vo-file
 	    (message "check compilation for module %s from object file %s"
 		     module-id module-vo-file)
@@ -1584,12 +1584,12 @@ might be used."
 	       (not (coq-compile-ignore-file module-vo-file)))
       (setq module-job
 	    (coq-par-create-library-job module-vo-file coq-load-path
-					coq-last-compilation-job span
+					coq--last-compilation-job span
 					"scripting buffer"))
-      (setq coq-last-compilation-job module-job)
-      (if coq-debug-auto-compilation
+      (setq coq--last-compilation-job module-job)
+      (if coq--debug-auto-compilation
 	  (message "%s: this job is the last compilation job now"
-		   (get coq-last-compilation-job 'name))))))
+		   (get coq--last-compilation-job 'name))))))
 
 (defun coq-par-handle-require-list (require-items)
   "Start compilation for the required modules in the car of REQUIRE-ITEMS.
@@ -1603,14 +1603,14 @@ to file names and creates one top-level compilation job for each
 required module that is not ignored (eg via
 `coq-compile-ignored-directories'). Jobs are started immediately
 if possible. The last such created job is remembered in
-`coq-last-compilation-job'. The REQUIRE-ITEMS are attached to
+`coq--last-compilation-job'. The REQUIRE-ITEMS are attached to
 this last top-level job or directly to proof-action-list, if
 there is no last compilation job."
   (let* ((item (car require-items))
 	 (string (mapconcat 'identity (nth 1 item) " "))
 	 (span (car item))
          prefix start)
-    (if coq-debug-auto-compilation
+    (if coq--debug-auto-compilation
 	(message "handle require command \"%s\"" string))
     ;; We know there is a require in string. But we have to match it
     ;; again in order to get the end position.
@@ -1626,22 +1626,22 @@ there is no last compilation job."
       (setq start (match-end 0))
       (coq-par-handle-module (match-string 1 string) span prefix))
     ;; add the asserted items to the last compilation job
-    (if coq-last-compilation-job
+    (if coq--last-compilation-job
 	(progn
-	  (assert (not (coq-par-job-is-ready coq-last-compilation-job))
+	  (assert (not (coq-par-job-is-ready coq--last-compilation-job))
 		  nil "last compilation job from previous compilation ready")
-	  (put coq-last-compilation-job 'queueitems
-	       (nconc (get coq-last-compilation-job 'queueitems)
+	  (put coq--last-compilation-job 'queueitems
+	       (nconc (get coq--last-compilation-job 'queueitems)
 		      require-items))
-	  (if coq-debug-auto-compilation
+	  (if coq--debug-auto-compilation
 	      (message "%s: attach %s items (containing now %s items)"
-		       (get coq-last-compilation-job 'name)
+		       (get coq--last-compilation-job 'name)
 		       (length require-items)
-		       (length (get coq-last-compilation-job 'queueitems)))))
+		       (length (get coq--last-compilation-job 'queueitems)))))
       ;; or add them directly to queueitems if there is no compilation job
       ;; (this happens if the modules are ignored for compilation)
       (setq queueitems (nconc queueitems require-items))
-      (if coq-debug-auto-compilation
+      (if coq--debug-auto-compilation
 	  (message "attach %s items to queueitems (containing now %s items)"
 		   (length require-items)
 		   (length queueitems))))))
@@ -1666,7 +1666,7 @@ If `coq-compile-before-require' is non-nil, this function starts
 the compilation (if necessary) of the dependencies
 ansynchronously in parallel in the background.
 
-If there is a last compilation job (`coq-last-compilation-job')
+If there is a last compilation job (`coq--last-compilation-job')
 then the queue region is extended, while some background
 compilation is still running. In this case I have to preserve the
 internal state. Otherwise the hash of the compilation jobs and
@@ -1684,51 +1684,51 @@ first of these batches, buffers are saved with
 Finally, `proof-second-action-list-active' is set if I keep some
 queue items because they have to wait for a compilation job. Then
 the maximal number of background compilation jobs is started."
-  (when coq-debug-auto-compilation
+  (when coq--debug-auto-compilation
     (message "%d items were added to the queue, scan for require"
 	     (length queueitems)))
-  (unless coq-last-compilation-job
+  (unless coq--last-compilation-job
     (coq-par-init-compilation-hash)
     (coq-par-init-ancestor-hash)
     (coq-init-compile-response-buffer))
   (let ((splitted-items
 	 (split-list-at-predicate queueitems
 				  'coq-par-item-require-predicate)))
-    (if coq-last-compilation-job
+    (if coq--last-compilation-job
 	(progn
-	  (put coq-last-compilation-job 'queueitems
-	       (nconc (get coq-last-compilation-job 'queueitems)
+	  (put coq--last-compilation-job 'queueitems
+	       (nconc (get coq--last-compilation-job 'queueitems)
 		      (car splitted-items)))
 	  (setq queueitems nil)
 	  (message "attach first %s items to job %s"
 		   (length (car splitted-items))
-		   (get coq-last-compilation-job 'name)))
+		   (get coq--last-compilation-job 'name)))
       (setq queueitems (car splitted-items))
-      (if coq-debug-auto-compilation
+      (if coq--debug-auto-compilation
 	  (message "attach first %s items directly to queue"
 		   (length (car splitted-items)))))
     ;; XXX handle external compilation here, compile everything
     ;; with one command, use compilation-finish-functions to get
     ;; notification
     (when (cdr splitted-items)
-      (when coq-compile-vio2vo-delay-timer
-	(cancel-timer coq-compile-vio2vo-delay-timer))
-      (when coq-compile-vio2vo-in-progress
-	(assert (not coq-last-compilation-job)
+      (when coq--compile-vio2vo-delay-timer
+	(cancel-timer coq--compile-vio2vo-delay-timer))
+      (when coq--compile-vio2vo-in-progress
+	(assert (not coq--last-compilation-job)
 		nil "normal compilation and vio2vo in parallel 2")
 	;; there are only vio2vo background processes
 	(coq-par-kill-all-processes)
-	(setq coq-compile-vio2vo-in-progress nil))
+	(setq coq--compile-vio2vo-in-progress nil))
       ;; save buffers before invoking the first coqdep
       (coq-compile-save-some-buffers)
       (mapc (lambda (require-items)
 	      (coq-par-handle-require-list require-items))
 	    (cdr splitted-items)))
-    (when coq-last-compilation-job
+    (when coq--last-compilation-job
       (setq proof-second-action-list-active t))
     (coq-par-start-jobs-until-full)
-    (if coq-debug-auto-compilation
-	(if coq-last-compilation-job
+    (if coq--debug-auto-compilation
+	(if coq--last-compilation-job
 	    (message "return control, waiting for background jobs")
 	  (message "return control, no background jobs")))))