Refactoring. New file coq-system.el.

3 files changed, 549 insertions, 527 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 2e8919f1..415f65ee 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -14,9 +14,10 @@
 
 
 (require 'proof-shell)
+(require 'coq-system)
 
 (eval-when (compile)
-  (defvar coq-pre-v85 nil)
+  ;;(defvar coq-pre-v85 nil)
   (defvar coq-confirm-external-compilation nil); defpacustom
   (defvar coq-compile-parallel-in-background nil) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
@@ -27,30 +28,6 @@
 ;; Multiple file handling -- sequential compilation of required modules
 ;;
 
-;; constants
-
-(defun get-coq-library-directory ()
-  (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 )))
-    (if (string-match "not found" c)
-        "/usr/local/lib/coq"
-      c)))
-
-(defconst coq-library-directory (get-coq-library-directory)
-  "The coq library directory, as reported by \"coqtop -where\".")
-
-(defcustom coq-dependency-analyzer
-  (proof-locate-executable "coqdep" t nil)
-  "Command to invoke coqdep."
-  :type 'string
-  :group 'coq)
-
-(defcustom coq-compiler
-  (proof-locate-executable "coqc" t nil)
-  "Command to invoke the coq compiler."
-  :type 'string
-  :group 'coq)
-
-
 ;;; enable / disable parallel / sequential compilation
 ;; I would rather put these functions into coq-seq-compile and
 ;; coq-par-compile, respectively. However, the :initialization
@@ -91,35 +68,6 @@ Must be used together with `coq-par-enable'."
 	       'coq-seq-preprocess-require-commands))
 
 
-;;; utility functions for variables
-
-(defun coq-load-path-safep (path)
-  "Check if PATH is a safe value for `coq-load-path'."
-  (and
-   (listp path)
-   (every
-    (lambda (entry)
-      (or (stringp entry)
-          (and (listp entry)
-               (eq (car entry) 'rec)
-               (every 'stringp (cdr entry))
-               (equal (length entry) 3))
-          (and (listp entry)
-               (eq (car entry) 'nonrec)
-               (every 'stringp (cdr entry))
-               (equal (length entry) 3))
-          (and (listp entry)
-               (eq (car entry) 'recnoimport)
-               (every 'stringp (cdr entry))
-               (equal (length entry) 3))
-          (and (listp entry)
-               (eq (car entry) 'ocamlimport)
-               (every 'stringp (cdr entry))
-               (equal (length entry) 2))
-          (and (listp entry)
-               (every 'stringp entry)
-               (equal (length entry) 2))))
-    path)))
 
 (defun coq-switch-compilation-method ()
   "Set function for coq-compile-parallel-in-background."
@@ -265,64 +213,6 @@ directory containing the source file, the Coq object file in
 identifier that occurs in the \"Require\" command, and the file
 that contains the \"Require\".")
 
-(defcustom coq-load-path nil
-  "Non-standard coq library load path.
-This list specifies the LoadPath extension for coqdep, coqc and
-coqtop. Usually, the elements of this list are strings (for
-\"-I\") or lists of two strings (for \"-R\" dir path and
-\"-Q\" dir path).
-
-The possible forms of elements of this list correspond to the 4
-forms of include options ('-I' '-Q' and '-R'). An element can be
-
-  - A list of the form '(ocamlimport dir)', specifying a
-    directory to be added to ocaml path ('-I').
-  - A list of the form '(rec dir path)' (where dir and path are
-    strings) specifying a directory to be recursively mapped to the
-    logical path 'path' ('-R dir path').
-  - A list of the form '(recnoimport dir path)' (where dir and
-    path are strings) specifying a directory to be recursively
-    mapped to the logical path 'path' ('-Q dir path'), but not
-    imported (modules accessible for import with qualified names
-    only).
-  - A list of the form '(norec dir)', specifying a directory
-    to be mapped to the empty logical path ('-Q dir \"\"').
-
-For convenience the symbol 'rec' can be omitted and entries of
-the form '(dir path)' are interpreted as '(rec dir path)'.
-
-Under normal circumstances this list does not need to
-contain the coq standard library or \".\" for the current
-directory (see `coq-load-path-include-current').
-
-WARNING: if you use coq <= 8.4, the meaning of these options is
-not the same (-I is for coq path).
-"
-  :type '(repeat (choice (string :tag "simple directory without path (-Q \"\")") ; is this really useful?
-                         (list :tag
-                               "recursive directory with path (-R ... -as ...)"
-                               (const rec)
-                               (string :tag "directory")
-                               (string :tag "log path"))
-			 (list :tag
-                               "recursive directory without recursive inport with path (-Q ... ...)"
-                               (const recnoimport)
-                               (string :tag "directory")
-                               (string :tag "log path"))
-                         (list :tag
-                               "directory with empty logical path (-Q ... "" in coq>=8.5, -I ... in coq<=8.4)"
-                               (const nonrec)
-                               (string :tag "directory")
-                               (string :tag "log path"))
-                         (list :tag
-                               "ocaml path (-I ...)"
-                               (const ocamlimport)
-                               (string :tag "directory")
-                               (string :tag "log path"))))
-  :safe 'coq-load-path-safep
-  :group 'coq-auto-compile)
-
-(make-variable-buffer-local 'coq-load-path)
 
 (defcustom coq-compile-auto-save 'ask-coq
   "Buffers to save before checking dependencies for compilation.
@@ -367,14 +257,6 @@ This option can be set/reset via menu
   :type 'boolean
   :group 'coq-auto-compile)
 
-(defcustom coq-load-path-include-current t
-  "If `t' let coqdep search the current directory too.
-Should be `t' for normal users. If `t' pass -Q dir \"\" to coqdep when
-processing files in directory \"dir\" in addition to any entries
-in `coq-load-path'."
-  :type 'boolean
-  :safe 'booleanp
-  :group 'coq-auto-compile)
 
 (defcustom coq-compile-ignored-directories nil
   "Directories in which ProofGeneral should not compile modules.
@@ -477,80 +359,7 @@ DEP-MOD-TIMES is empty it returns nil."
 
 ;;; Compute command line for starting coqtop
 
-(defun coq-option-of-load-path-entry (entry)
-  "Translate a single element from `coq-load-path' into options.
-See `coq-load-path' for the possible forms of entry and to which
-options they are translated."
-  (cond
-   ((and coq-pre-v85 (stringp entry))
-    (list "-I" (expand-file-name entry)))
-   ((and (not coq-pre-v85) (stringp entry))
-    (list "-Q" (expand-file-name entry) ""))
-   ((and coq-pre-v85 (eq (car entry) 'nonrec))
-    (list "-I" (expand-file-name (nth 1 entry)) "-as" (nth 2 entry)))
-   ((and (not coq-pre-v85) (eq (car entry) 'nonrec)) ;; N/A?
-    (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry)))
-   ((eq (car entry) 'recnoimport) ;; only for >=8.5
-    (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry)))
-   (t
-    (if (eq (car entry) 'rec)
-        (setq entry (cdr entry)))
-    (if coq-pre-v85 ;; -as obsolete in 8.5
-	(list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry))
-      (list "-R" (expand-file-name (car entry)) (nth 1 entry))))))
-
-
-(defun coq-include-options (file coq-load-path)
-  "Build the list of include options for coqc, coqdep and coqtop.
-The options list includes all entries from argument COQ-LOAD-PATH
-\(which should be `coq-load-path' of the buffer that invoked the
-compilation) prefixed with suitable options and (for coq<8.5), if
-`coq-load-path-include-current' is enabled, the directory base of
-FILE. The resulting list is fresh for every call, callers can
-append more 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))
-    (unless (coq-load-path-safep coq-load-path)
-      (error "Invalid value in coq-load-path"))
-    (when coq-load-path
-      (setq result (coq-option-of-load-path-entry (car coq-load-path)))
-      (dolist (entry (cdr coq-load-path))
-        (nconc result (coq-option-of-load-path-entry entry))))
-    (if coq-load-path-include-current
-        (setq result
-              (if coq-pre-v85
-		  (cons "-I" (cons (file-name-directory file) result))
-		;; from coq-8.5 beta3 cpqdep does not needthis anymore
-		;; and actually it can clash with -Q . foo written in
-		;; _CoqProject
-		;; (cons "-Q" (cons (file-name-directory file) (cons "" result)))
-		result)))
-    result))
-
-
-(defun coq-coqdep-prog-args (&optional src-file loadpath)
-  (let ((loadpath (or loadpath coq-load-path)))
-    (coq-include-options src-file loadpath)))
-
-(defun coq-coqc-prog-args (&optional src-file loadpath)
-  ;; coqtop always adds the current directory to the LoadPath, so don't
-  ;; include it in the -Q options.
-  (let ((coqdep-args
-	 (let ((coq-load-path-include-current nil)) ; obsolete >=8.5beta3
-	   (append coq-prog-args (coq-coqdep-prog-args src-file loadpath)))))
-    (remove "-emacs" (remove "-emacs-U" coqdep-args))))
-
-(defun coq-coqtop-prog-args (&optional src-file loadpath)
-  ;; coqtop always adds the current directory to the LoadPath, so don't
-  ;; include it in the -Q options. This is not true for coqdep.
-  (cons "-emacs" (coq-coqc-prog-args src-file loadpath)))
-
-;; FIXME: we seem to need this function with this exact name,
-;; otherwise coqtop command is not generated with the good load-path
-;; (??). Is it interfering with defpgcustom's in pg-custom.el?
-(defun coq-prog-args () (coq-coqtop-prog-args))
+
 
 
 
diff --git a/coq/coq-system.el b/coq/coq-system.el
new file mode 100644
index 00000000..a8e2f1af
--- /dev/null
+++ b/coq/coq-system.el
@@ -0,0 +1,532 @@
+;; coq-system.el --- common part of compilation feature
+;; Copyright (C) 2015 LFCS Edinburgh.
+;; Authors: Hendrik Tews, Pierre Courtieu
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+;; Maintainer: Pierre.Courtieu<Pierre.Courtieu@cnam.fr>
+;;
+
+;;; Commentary:
+;;
+;; This file holds constants, options and some general functions for
+;; setting coq command arguments. Some code is dedicated as a light
+;; support for older versions of coq.
+;;
+
+(require 'proof)
+
+(eval-when-compile
+  (require 'cl)
+  (require 'proof-compat)
+  (proof-ready-for-assistant 'coq))
+
+(eval-when (compile)
+  (defvar coq-prog-args nil)
+  (defvar coq-debug nil))
+
+(eval-when (compile)
+  (defvar coq-pre-v85 nil))
+
+(defun get-coq-version ()
+  (let ((c (shell-command-to-string "coqtop -v")))
+    (if (string-match "version \\([^ ]+\\)\\s-" c)
+	(match-string 1 c)
+      c)))
+
+
+(defcustom coq-prog-env nil
+  "List of environment settings d to pass to Coq process.
+On Windows you might need something like:
+  (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
+  :group 'coq)
+
+(defcustom coq-prog-name
+  (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))
+   "*Name of program to run as Coq. See `proof-prog-name', set from this.
+On Windows with latest Coq package you might need something like:
+   C:/Program Files/Coq/bin/coqtop.opt.exe
+instead of just \"coqtop\".
+This must be a single program name with no arguments; see `coq-prog-args'
+to manually adjust the arguments to the Coq process.
+See also `coq-prog-env' to adjust the environment."
+   :type 'string
+   :group 'coq)
+
+(defcustom coq-dependency-analyzer
+  (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin"))
+  "Command to invoke coqdep."
+  :type 'string
+  :group 'coq)
+
+(defcustom coq-compiler
+  (proof-locate-executable "coqc" t '("C:/Program Files/Coq/bin"))
+  "Command to invoke the coq compiler."
+  :type 'string
+  :group 'coq)
+
+(defun get-coq-library-directory ()
+  (let ((c (substring (shell-command-to-string (concat coq-prog-name " -where")) 0 -1 )))
+    (if (string-match "not found" c)
+        "/usr/local/lib/coq"
+      c)))
+
+(defconst coq-library-directory (get-coq-library-directory)
+  "The coq library directory, as reported by \"coqtop -where\".")
+
+(defcustom coq-tags (concat coq-library-directory "/theories/TAGS")
+  "The default TAGS table for the Coq library."
+  :type 'string
+  :group 'coq)
+
+(defcustom coq-pre-v85 nil
+  "Whether to use <= coq-8.4 config (nil by default).
+Mainly to deal with command line options that changed between 8.4
+and 8.5 (-Q foo bar replace -I foo)."
+  :type 'boolean
+  :group 'coq)
+
+(defcustom coq-use-makefile nil
+  "Whether to look for a Makefile to attempt to guess the command line.
+Set to t if you want this feature."
+  :type 'string
+  :group 'coq)
+
+(defcustom coq-www-home-page "http://coq.inria.fr/"
+  "Coq home page URL."
+  :type 'string
+  :group 'coq)
+
+;;; utility functions for variables
+
+(defun coq-load-path-safep (path)
+  "Check if PATH is a safe value for `coq-load-path'."
+  (and
+   (listp path)
+   (every
+    (lambda (entry)
+      (or (stringp entry)
+          (and (listp entry)
+               (eq (car entry) 'rec)
+               (every 'stringp (cdr entry))
+               (equal (length entry) 3))
+          (and (listp entry)
+               (eq (car entry) 'nonrec)
+               (every 'stringp (cdr entry))
+               (equal (length entry) 3))
+          (and (listp entry)
+               (eq (car entry) 'recnoimport)
+               (every 'stringp (cdr entry))
+               (equal (length entry) 3))
+          (and (listp entry)
+               (eq (car entry) 'ocamlimport)
+               (every 'stringp (cdr entry))
+               (equal (length entry) 2))
+          (and (listp entry)
+               (every 'stringp entry)
+               (equal (length entry) 2))))
+    path)))
+
+(defcustom coq-load-path nil
+  "Non-standard coq library load path.
+This list specifies the LoadPath extension for coqdep, coqc and
+coqtop. Usually, the elements of this list are strings (for
+\"-I\") or lists of two strings (for \"-R\" dir path and
+\"-Q\" dir path).
+
+The possible forms of elements of this list correspond to the 4
+forms of include options ('-I' '-Q' and '-R'). An element can be
+
+  - A list of the form '(ocamlimport dir)', specifying a
+    directory to be added to ocaml path ('-I').
+  - A list of the form '(rec dir path)' (where dir and path are
+    strings) specifying a directory to be recursively mapped to the
+    logical path 'path' ('-R dir path').
+  - A list of the form '(recnoimport dir path)' (where dir and
+    path are strings) specifying a directory to be recursively
+    mapped to the logical path 'path' ('-Q dir path'), but not
+    imported (modules accessible for import with qualified names
+    only).
+  - A list of the form '(norec dir)', specifying a directory
+    to be mapped to the empty logical path ('-Q dir \"\"').
+
+For convenience the symbol 'rec' can be omitted and entries of
+the form '(dir path)' are interpreted as '(rec dir path)'.
+
+Under normal circumstances this list does not need to
+contain the coq standard library or \".\" for the current
+directory (see `coq-load-path-include-current').
+
+WARNING: if you use coq <= 8.4, the meaning of these options is
+not the same (-I is for coq path).
+"
+  :type '(repeat (choice (string :tag "simple directory without path (-Q \"\")") ; is this really useful?
+                         (list :tag
+                               "recursive directory with path (-R ... -as ...)"
+                               (const rec)
+                               (string :tag "directory")
+                               (string :tag "log path"))
+			 (list :tag
+                               "recursive directory without recursive inport with path (-Q ... ...)"
+                               (const recnoimport)
+                               (string :tag "directory")
+                               (string :tag "log path"))
+                         (list :tag
+                               "directory with empty logical path (-Q ... "" in coq>=8.5, -I ... in coq<=8.4)"
+                               (const nonrec)
+                               (string :tag "directory")
+                               (string :tag "log path"))
+                         (list :tag
+                               "ocaml path (-I ...)"
+                               (const ocamlimport)
+                               (string :tag "directory")
+                               (string :tag "log path"))))
+  :safe 'coq-load-path-safep
+  :group 'coq-auto-compile)
+
+(make-variable-buffer-local 'coq-load-path)
+
+(defcustom coq-load-path-include-current t
+  "If `t' let coqdep search the current directory too.
+Should be `t' for normal users. If `t' pass -Q dir \"\" to coqdep when
+processing files in directory \"dir\" in addition to any entries
+in `coq-load-path'."
+  :type 'boolean
+  :safe 'booleanp
+  :group 'coq-auto-compile)
+
+(defun coq-option-of-load-path-entry (entry)
+  "Translate a single element from `coq-load-path' into options.
+See `coq-load-path' for the possible forms of entry and to which
+options they are translated."
+  (cond
+   ((and coq-pre-v85 (stringp entry))
+    (list "-I" (expand-file-name entry)))
+   ((and (not coq-pre-v85) (stringp entry))
+    (list "-Q" (expand-file-name entry) ""))
+   ((and coq-pre-v85 (eq (car entry) 'nonrec))
+    (list "-I" (expand-file-name (nth 1 entry)) "-as" (nth 2 entry)))
+   ((and (not coq-pre-v85) (eq (car entry) 'nonrec)) ;; N/A?
+    (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry)))
+   ((eq (car entry) 'recnoimport) ;; only for >=8.5
+    (list "-Q" (expand-file-name (nth 1 entry)) (nth 2 entry)))
+   (t
+    (if (eq (car entry) 'rec)
+        (setq entry (cdr entry)))
+    (if coq-pre-v85 ;; -as obsolete in 8.5
+	(list "-R" (expand-file-name (car entry)) "-as" (nth 1 entry))
+      (list "-R" (expand-file-name (car entry)) (nth 1 entry))))))
+
+(defun coq-include-options (file coq-load-path)
+  "Build the list of include options for coqc, coqdep and coqtop.
+The options list includes all entries from argument COQ-LOAD-PATH
+\(which should be `coq-load-path' of the buffer that invoked the
+compilation) prefixed with suitable options and (for coq<8.5), if
+`coq-load-path-include-current' is enabled, the directory base of
+FILE. The resulting list is fresh for every call, callers can
+append more 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))
+    (unless (coq-load-path-safep coq-load-path)
+      (error "Invalid value in coq-load-path"))
+    (when coq-load-path
+      (setq result (coq-option-of-load-path-entry (car coq-load-path)))
+      (dolist (entry (cdr coq-load-path))
+        (nconc result (coq-option-of-load-path-entry entry))))
+    (if coq-load-path-include-current
+        (setq result
+              (if coq-pre-v85
+		  (cons "-I" (cons (file-name-directory file) result))
+		;; from coq-8.5 beta3 cpqdep does not needthis anymore
+		;; and actually it can clash with -Q . foo written in
+		;; _CoqProject
+		;; (cons "-Q" (cons (file-name-directory file) (cons "" result)))
+		result)))
+    result))
+
+
+
+(defun coq-coqdep-prog-args (&optional src-file loadpath)
+  (let ((loadpath (or loadpath coq-load-path)))
+    (coq-include-options src-file loadpath)))
+
+(defun coq-coqc-prog-args (&optional src-file loadpath)
+  ;; coqtop always adds the current directory to the LoadPath, so don't
+  ;; include it in the -Q options.
+  (let ((coqdep-args
+	 (let ((coq-load-path-include-current nil)) ; obsolete >=8.5beta3
+	   ;; by the time this function is called, coq-prog-args should be set 
+	   (append coq-prog-args
+		   (coq-coqdep-prog-args src-file loadpath)))))
+    (remove "-emacs" (remove "-emacs-U" coqdep-args))))
+
+;;XXXXXXXXXXXXXX
+;; coq-coqtop-prog-args is the user-set list of arguments to pass to
+;; Coq process, see 'defpacustom prog-args' in pg-custom.el for
+;; documentation.
+
+(defun coq-coqtop-prog-args (&optional src-file loadpath)
+  ;; coqtop always adds the current directory to the LoadPath, so don't
+  ;; include it in the -Q options. This is not true for coqdep.
+  (cons "-emacs" (coq-coqc-prog-args src-file loadpath)))
+
+;; FIXME: we seem to need this function with this exact name,
+;; otherwise coqtop command is not generated with the good load-path
+;; (??). Is it interfering with defpgcustom's in pg-custom.el?
+(defun coq-prog-args () (coq-coqtop-prog-args))
+
+
+
+(defcustom coq-use-project-file t
+  "If t, when opening a coq file read the dominating _CoqProject.
+If t when a coq file is opened, proofgeneral will look for a
+project file (see `coq-project-filename') somewhere in the
+current directory or its parents directory. If there is one, its
+content is read and used to determine the arguments that must be
+given to coqtop. In particular it sets the load path (including
+the -R lib options) (see `coq-load-path') ."
+  :type 'boolean
+  :group 'coq)
+
+(defcustom coq-project-filename "_CoqProject"
+  "The name of coq project file.
+The coq project file of a coq developpement (Cf Coq documentation
+on \"makefile generation\") should contain the arguments given to
+coq_makefile. In particular it contains the -I and -R
+options (one per line). If `coq-use-coqproject' is t (default)
+the content of this file will be used by proofgeneral to infer
+the `coq-load-path' and the `coq-prog-args' variables that set
+the coqtop invocation by proofgeneral. This is now the
+recommended way of configuring the coqtop invocation. Local file
+variables may still be used to override the coq project file's
+configuration. .dir-locals.el files also work and override
+project file settings."
+  :type 'string
+  :group 'coq)
+
+
+(defun coq-find-project-file ()
+  "Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
+alreadyopen is t if buffer already existed."
+  (let* (
+         (projectfiledir (locate-dominating-file buffer-file-name coq-project-filename)))
+    (when projectfiledir
+      (let* ((projectfile (expand-file-name coq-project-filename projectfiledir))
+             ;; we store this intermediate result to know if we have to kill
+             ;; the coq project buffer at the end
+             (projectbufferalreadyopen (find-buffer-visiting projectfile))
+             (projectbuffer (or projectbufferalreadyopen
+                                (find-file-noselect projectfile t t))))
+        (list projectbuffer projectbufferalreadyopen)))))
+
+;; No "." no "-" in coq module file names, but we do not check
+;; TODO: look exactly at what characters are allowed.
+(defconst coq-load-path--R-regexp
+  "\\_<-R\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)")
+
+(defconst coq-load-path--Q-regexp
+  "\\_<-Q\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)")
+
+;; second arg of -I is optional (and should become obsolete one day)
+(defconst coq-load-path--I-regexp
+  "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)\\(?:[:space:]+\\(?2:[^[:space:]]+\\)\\)?")
+
+;(defconst coq-load-path--I-regexp "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)")
+
+;; match-string 1 must contain the string to add to coqtop command line, so we
+;; ignore -arg, we use numbered subregexpr.
+
+;; FIXME: if several options are given (within "") in a single -arg line, then
+;; they are glued and passed as a single argument to coqtop. this is bad and
+;; not conforming to coq_makefile. HOWEVER: this is probably a bad feature of
+;; coq_makefile to allow several arguments in a single - arg "xxx yyy".
+(defconst coq-prog-args-regexp
+  "\\_<\\(?1:-opt\\|-byte\\)\\|-arg[[:space:]]+\\(?:\\(?1:[^\"\t\n#]+\\)\\|\"\\(?1:[^\"]+\\)\"\\)")
+
+
+(defun coq-read-option-from-project-file (projectbuffer regexp &optional dirprefix)
+  "look for occurrences of regexp in buffer projectbuffer and collect subexps.
+The returned sub-regexp are the one numbered 1 and 2 (other ones
+should be unnumbered). If there is only subexp 1 then it is added
+as is to the final list, if there are 1 and 2 then a list
+containing both is added to the final list. If optional DIRPREFIX
+is non nil, then options ar considered as directory or file names
+and will be made absolute from directory named DIRPREFIX. This
+allows to call coqtop from a subdirectory of the project."
+  (let ((opt nil))
+    (when projectbuffer
+      (with-current-buffer projectbuffer
+        (goto-char (point-min))
+        (while (re-search-forward regexp nil t)
+          (let* ((firstfname (match-string 1))
+                 (second (match-string 2))
+                 (first (if (null dirprefix) firstfname
+                          (expand-file-name firstfname dirprefix))))
+            (if second ; if second arg is "" (two doublequotes), it means empty string
+                (let ((sec (if (string-equal second "\"\"") "" second)))
+                  (if (string-match coq-load-path--R-regexp (match-string 0))
+                      (setq opt (cons (list first sec) opt))
+                    (setq opt (cons (list 'recnoimport first sec) opt))))
+              (setq opt (cons first opt))))))
+      (reverse opt))))
+
+;; Look for -R and -I options in the project buffer
+;; add the default "." too
+(defun coq-search-load-path (projectbuffer)
+  "Read project buffer and retrurn a value for `coq-load-path'."
+;;  no automatic insertion of "." here because some people want to do "-R . foo" so
+;;  let us avoid conflicts.
+  (coq-read-option-from-project-file
+   projectbuffer
+   (concat coq-load-path--R-regexp "\\|" coq-load-path--Q-regexp "\\|" coq-load-path--I-regexp)
+   (file-name-directory (buffer-file-name projectbuffer))))
+
+;; Look for other options (like -opt, -arg foo etc) in the project buffer
+;; adds the -emacs option too
+(defun coq-search-prog-args (projectbuffer)
+  "Read project buffer and retrurn a value for `coq-prog-args'"
+  (cons
+   "-emacs"
+   (coq-read-option-from-project-file projectbuffer coq-prog-args-regexp)))
+
+
+;; optional args allow to implement the precedence of dir/file local vars
+(defun coq-load-project-file-with-avoid (&optional avoidargs avoidpath)
+  (let* ((projectbuffer-aux (coq-find-project-file))
+         (projectbuffer (and projectbuffer-aux (car projectbuffer-aux)))
+         (no-kill (and projectbuffer-aux (car (cdr projectbuffer-aux)))))
+    (if (not projectbuffer-aux)
+        (message "Coq project file not detected.")
+      (unless avoidargs (setq coq-prog-args (coq-search-prog-args projectbuffer)))
+      (unless avoidpath (setq coq-load-path (coq-search-load-path projectbuffer)))
+      (let ((msg
+             (cond
+              ((and avoidpath avoidargs) "Coqtop args and load path")
+              (avoidpath "Coqtop load path")
+              (avoidargs "Coqtop args")
+              (t ""))))
+        (message
+         "Coq project file detected: %s%s." (buffer-file-name projectbuffer)
+         (if (or avoidpath avoidargs)
+             (concat "\n(" msg " overridden by dir/file local values)")
+           "")))
+      (when coq-debug
+        (message "coq-prog-args: %S" coq-prog-args)
+        (message "coq-load-path: %S" coq-load-path))
+      (unless no-kill (kill-buffer projectbuffer)))))
+
+
+
+(defun coq-load-project-file ()
+  "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file.
+Obeys `coq-use-project-file'. Note that if a variable is already
+set by dir/file local variables, this function will not override
+its value.
+See `coq-project-filename' to change the name of the
+project file, and `coq-use-project-file' to disable this
+feature."
+  (when coq-use-project-file
+    ;; Let us reread dir/file local vars, in case the user mmodified them
+    (let* ((oldargs (assoc 'coq-prog-args file-local-variables-alist))
+           (oldpath (assoc 'coq-load-path file-local-variables-alist)))
+      (coq-load-project-file-with-avoid oldargs oldpath))))
+
+
+(defun coq-load-project-file-rehack ()
+  "Reread file/dir local vars and call `coq-load-project-file'.
+Does nothing if `coq-use-project-file' is nil.
+Warning: 
+"
+  (when coq-use-project-file
+    ;; Let us reread dir/file local vars, in case the user mmodified them
+    (hack-local-variables)
+    ;; Useless since coq-load-project-file is in hack-local-variables-hook:
+    ;;(coq-load-project-file)
+    ))
+
+
+;; Since coq-project-filename can be set via .dir-locals.el or file variable,
+;; we need to call coq-load-coq-project-file only *after* local variables are
+;; set. But coq-mode-hook is called BEFORE local variables are read. Therefore
+;; coq-load-coq-project-file is added to hack-local-variables-hook instead. To
+;; avoid adding for other modes , the setting is performed inside
+;; coq-mode-hook. This is described in www.emacswiki.org/emacs/LocalVariables
+
+;; TODO: also read COQBIN somewhere?
+;; Note: this does not need to be at a particular place in the hook, but we
+;; need to make this hook local.
+;; hack-local-variables-hook seems to hack local and dir local vars.
+(add-hook 'coq-mode-hook
+          '(lambda ()
+             (add-hook 'hack-local-variables-hook
+                       'coq-load-project-file
+                       nil t)))
+
+;; smie's parenthesis blinking is too slow, let us have the default one back
+(add-hook 'coq-mode-hook
+          '(lambda ()
+             (when (and (fboundp 'show-paren--default)
+                        (boundp 'show-paren-data-function))
+               (setq show-paren-data-function 'show-paren--default))))
+
+
+
+(defun coq-toggle-use-project-file ()
+  (interactive)
+  (setq coq-use-project-file (not coq-use-project-file))
+  (when coq-use-project-file (coq-load-project-file-rehack))
+  ;; FIXME What should we do when disabling project file? since
+  ;; local variables override project file anyway, reading them
+  ;; again is useless. Let us do nothing.
+  ;;(setq coq-load-path nil)
+  ;;(setq coq-prog-args nil)
+  )
+
+
+(provide 'coq-system)
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;    To guess the command line options   ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; OBSOLETE, should take _CoqProject into account.
+(defun coq-guess-command-line (filename)
+  "Guess the right command line options to compile FILENAME using `make -n'.
+This function is obsolete, the recommended way of setting the
+coqtop options is to use a _Coqproject file as described in coq
+documentation. ProofGeneral reads this file and sets compilation
+options according to its contents. See `coq-project-filename'. Per file configuration may
+then be set using local file variables."
+  (if (local-variable-p 'coq-prog-name (current-buffer))
+      coq-prog-name
+    (let* ((dir (or (file-name-directory filename) "."))
+           (makedir
+           (cond
+            ((file-exists-p (concat dir "Makefile")) ".")
+            ;; ((file-exists-p (concat dir "../Makefile")) "..")
+            ;; ((file-exists-p (concat dir "../../Makefile")) "../..")
+            (t nil))))
+      (if (and coq-use-makefile makedir)
+          (let*
+              ;;TODO, add dir name when makefile is in .. or ../..
+              ;;
+              ;; da: FIXME: this code causes problems if the make
+              ;; command fails.  It should not be used by default
+              ;; and should be made more robust.
+              ;;
+              ((compiled-file (concat (substring
+                                       filename 0
+                                       (string-match ".v$" filename)) ".vo"))
+               (command (shell-command-to-string
+                         (concat  "cd " dir ";"
+                                  "make -n -W " filename " " compiled-file
+                                  "| sed s/coqc/coqtop/"))))
+            (message command)
+            (setq coq-prog-args nil)
+            (concat
+             (substring command 0 (string-match " [^ ]*$" command))
+             "-emacs-U"))
+        coq-prog-name))))
+
+;;; coq-compile-common.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index a08ca3f4..69c81194 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -32,9 +32,10 @@
   (proof-ready-for-assistant 'coq))     ; compile for coq
 
 (require 'proof)
-(require 'coq-syntax)                   ; sets coq-prog-name
-(require 'coq-local-vars)               ;
-(require 'coq-abbrev)                   ; coq specific menu
+(require 'coq-system)                   ; load path, option, project file etc.
+(require 'coq-syntax)
+(require 'coq-local-vars)               
+(require 'coq-abbrev)                   ; abbrev and  coq specific menu
 (require 'coq-seq-compile)              ; sequential compilation
 (require 'coq-par-compile)              ; parallel compilation
 
@@ -59,13 +60,6 @@
     (defvar prettify-symbols-alist nil)))
 
 
-(defun get-coq-version ()
-  (let ((c (shell-command-to-string "coqtop -v")))
-    (if (string-match "version \\([^ ]+\\)\\s-" c)
-	(match-string 1 c)
-      c)))
-
-
 ;; ----- coq-shell configuration options
 
 ;;; Code:
@@ -74,47 +68,11 @@
 (defvar coq-debug nil)
 ;; End debugging
 
-(defcustom coq-prog-name
-  (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin"))
-   "*Name of program to run as Coq. See `proof-prog-name', set from this.
-On Windows with latest Coq package you might need something like:
-   C:/Program Files/Coq/bin/coqtop.opt.exe
-instead of just \"coqtop\".
-This must be a single program name with no arguments; see `coq-prog-args'
-to manually adjust the arguments to the Coq process.
-See also `coq-prog-env' to adjust the environment."
-   :type 'string
-   :group 'coq)
-
-;; coq-prog-args is the user-set list of arguments to pass to Coq process,
-;; see 'defpacustom prog-args' in pg-custom.el for documentation.
-
-;; For Coq, this should contain -emacs.
-;; -translate will be added automatically to this list if `coq-translate-to-v8'
-;; is set.  The list is not altered if the user has set this herself.
-
-(defcustom coq-translate-to-v8 nil
-  "Whether to use -translate argument to Coq."
-  :type 'boolean
-  :group 'coq)
-
-(defcustom coq-pre-v85 nil
-  "Whether to use <= coq-8.4 config (nil by default).
-Mainly to deal with command line options that changed between 8.4
-and 8.5 (-Q foo bar replace -I foo)."
-  :type 'boolean
-  :group 'coq)
-
-(defcustom coq-use-makefile nil
-  "Whether to look for a Makefile to attempt to guess the command line.
-Set to t if you want this feature."
-  :type 'string
-  :group 'coq)
-
-(defcustom coq-default-undo-limit 500
-  "Maximum number of Undo's possible when doing a proof."
-  :type 'number
-  :group 'coq)
+;; Obsolete
+;;(defcustom coq-default-undo-limit 500
+;;  "Maximum number of Undo's possible when doing a proof."
+;;  :type 'number
+;;  :group 'coq)
 
 (defcustom coq-user-init-cmd nil
   "user defined init commands for Coq.
@@ -147,12 +105,6 @@ These are appended at the end of `coq-shell-init-cmd'."
 ;; coq-script-parse-cmdend-forward/backward and coq-find-real-start.
 (require 'coq-indent)
 
-(defcustom coq-prog-env nil
-  "List of environment settings d to pass to Coq process.
-On Windows you might need something like:
-  (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
-  :group 'coq)
-
 
 ;; Command to reset the Coq Proof Assistant
 (defconst coq-shell-restart-cmd "Reset Initial.\n ")
@@ -176,19 +128,9 @@ On Windows you might need something like:
   "\\(============================\\)\\|\\(subgoal [0-9]+\\)\n")
 
 
-(defcustom coq-tags (concat coq-library-directory "/theories/TAGS")
-  "The default TAGS table for the Coq library."
-  :type 'string
-  :group 'coq)
-
 (defconst coq-interrupt-regexp "User Interrupt."
   "Regexp corresponding to an interrupt.")
 
-(defcustom coq-www-home-page "http://coq.inria.fr/"
-  "Coq home page URL."
-  :type 'string
-  :group 'coq)
-
 (defcustom coq-end-goals-regexp-show-subgoals "\n(dependent evars:"
   "Regexp for `proof-shell-end-goals-regexp' when showing all subgoals.
 A setting of nil means show all output from Coq. See also
@@ -1309,253 +1251,8 @@ goal is redisplayed."
     (compile (concat "make " (substring n 0 l) ".vo"))))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;    To guess the command line options   ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun coq-guess-command-line (filename)
-  "Guess the right command line options to compile FILENAME using `make -n'.
-This function is obsolete, the recommended way of setting the
-coqtop options is to use a _Coqproject file as described in coq
-documentation. ProofGeneral reads this file and sets compilation
-options according to its contents. See `coq-project-filename'. Per file configuration may
-then be set using local file variables."
-  (if (local-variable-p 'coq-prog-name (current-buffer))
-      coq-prog-name
-    (let* ((dir (or (file-name-directory filename) "."))
-           (makedir
-           (cond
-            ((file-exists-p (concat dir "Makefile")) ".")
-            ;; ((file-exists-p (concat dir "../Makefile")) "..")
-            ;; ((file-exists-p (concat dir "../../Makefile")) "../..")
-            (t nil))))
-      (if (and coq-use-makefile makedir)
-          (let*
-              ;;TODO, add dir name when makefile is in .. or ../..
-              ;;
-              ;; da: FIXME: this code causes problems if the make
-              ;; command fails.  It should not be used by default
-              ;; and should be made more robust.
-              ;;
-              ((compiled-file (concat (substring
-                                       filename 0
-                                       (string-match ".v$" filename)) ".vo"))
-               (command (shell-command-to-string
-                         (concat  "cd " dir ";"
-                                  "make -n -W " filename " " compiled-file
-                                  "| sed s/coqc/coqtop/"))))
-            (message command)
-            (setq coq-prog-args nil)
-            (concat
-             (substring command 0 (string-match " [^ ]*$" command))
-             "-emacs-U"))
-        coq-prog-name))))
-
-
-(defcustom coq-use-project-file t
-  "If t, when opening a coq file read the dominating _CoqProject.
-If t when a coq file is opened, proofgeneral will look for a
-project file (see `coq-project-filename') somewhere in the
-current directory or its parents directory. If there is one, its
-content is read and used to determine the arguments that must be
-given to coqtop. In particular it sets the load path (including
-the -R lib options) (see `coq-load-path') ."
-  :type 'boolean
-  :group 'coq)
-
-(defcustom coq-project-filename "_CoqProject"
-  "The name of coq project file.
-The coq project file of a coq developpement (Cf Coq documentation
-on \"makefile generation\") should contain the arguments given to
-coq_makefile. In particular it contains the -I and -R
-options (one per line). If `coq-use-coqproject' is t (default)
-the content of this file will be used by proofgeneral to infer
-the `coq-load-path' and the `coq-prog-args' variables that set
-the coqtop invocation by proofgeneral. This is now the
-recommended way of configuring the coqtop invocation. Local file
-variables may still be used to override the coq project file's
-configuration. .dir-locals.el files also work and override
-project file settings."
-  :type 'string)
-
-
-(defun coq-find-project-file ()
-  "Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
-alreadyopen is t if buffer already existed."
-  (let* (
-         (projectfiledir (locate-dominating-file buffer-file-name coq-project-filename)))
-    (when projectfiledir
-      (let* ((projectfile (expand-file-name coq-project-filename projectfiledir))
-             ;; we store this intermediate result to know if we have to kill
-             ;; the coq project buffer at the end
-             (projectbufferalreadyopen (find-buffer-visiting projectfile))
-             (projectbuffer (or projectbufferalreadyopen
-                                (find-file-noselect projectfile t t))))
-        (list projectbuffer projectbufferalreadyopen)))))
-
-;; No "." no "-" in coq module file names, but we do not check
-;; TODO: look exactly at what characters are allowed.
-(defconst coq-load-path--R-regexp
-  "\\_<-R\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)")
-
-(defconst coq-load-path--Q-regexp
-  "\\_<-Q\\s-+\\(?1:[^[:space:]]+\\)\\s-+\\(?2:[^[:space:]]+\\)")
-
-;; second arg of -I is optional (and should become obsolete one day)
-(defconst coq-load-path--I-regexp
-  "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)\\(?:[:space:]+\\(?2:[^[:space:]]+\\)\\)?")
-
-;(defconst coq-load-path--I-regexp "\\_<-I\\s-+\\(?1:[^[:space:]]+\\)")
-
-;; match-string 1 must contain the string to add to coqtop command line, so we
-;; ignore -arg, we use numbered subregexpr.
-
-;; FIXME: if several options are given (within "") in a single -arg line, then
-;; they are glued and passed as a single argument to coqtop. this is bad and
-;; not conforming to coq_makefile. HOWEVER: this is probably a bad feature of
-;; coq_makefile to allow several arguments in a single - arg "xxx yyy".
-(defconst coq-prog-args-regexp
-  "\\_<\\(?1:-opt\\|-byte\\)\\|-arg[[:space:]]+\\(?:\\(?1:[^\"\t\n#]+\\)\\|\"\\(?1:[^\"]+\\)\"\\)")
-
-
-(defun coq-read-option-from-project-file (projectbuffer regexp &optional dirprefix)
-  "look for occurrences of regexp in buffer projectbuffer and collect subexps.
-The returned sub-regexp are the one numbered 1 and 2 (other ones
-should be unnumbered). If there is only subexp 1 then it is added
-as is to the final list, if there are 1 and 2 then a list
-containing both is added to the final list. If optional DIRPREFIX
-is non nil, then options ar considered as directory or file names
-and will be made absolute from directory named DIRPREFIX. This
-allows to call coqtop from a subdirectory of the project."
-  (let ((opt nil))
-    (when projectbuffer
-      (with-current-buffer projectbuffer
-        (goto-char (point-min))
-        (while (re-search-forward regexp nil t)
-          (let* ((firstfname (match-string 1))
-                 (second (match-string 2))
-                 (first (if (null dirprefix) firstfname
-                          (expand-file-name firstfname dirprefix))))
-            (if second ; if second arg is "" (two doublequotes), it means empty string
-                (let ((sec (if (string-equal second "\"\"") "" second)))
-                  (if (string-match coq-load-path--R-regexp (match-string 0))
-                      (setq opt (cons (list first sec) opt))
-                    (setq opt (cons (list 'recnoimport first sec) opt))))
-              (setq opt (cons first opt))))))
-      (reverse opt))))
-
-;; Look for -R and -I options in the project buffer
-;; add the default "." too
-(defun coq-search-load-path (projectbuffer)
-  "Read project buffer and retrurn a value for `coq-load-path'."
-;;  no automatic insertion of "." here because some people want to do "-R . foo" so
-;;  let us avoid conflicts.
-  (coq-read-option-from-project-file
-   projectbuffer
-   (concat coq-load-path--R-regexp "\\|" coq-load-path--Q-regexp "\\|" coq-load-path--I-regexp)
-   (file-name-directory (buffer-file-name projectbuffer))))
-
-;; Look for other options (like -opt, -arg foo etc) in the project buffer
-;; adds the -emacs option too
-(defun coq-search-prog-args (projectbuffer)
-  "Read project buffer and retrurn a value for `coq-prog-args'"
-  (cons
-   "-emacs"
-   (coq-read-option-from-project-file projectbuffer coq-prog-args-regexp)))
-
-
-;; optional args allow to implement the precedence of dir/file local vars
-(defun coq-load-project-file-with-avoid (&optional avoidargs avoidpath)
-  (let* ((projectbuffer-aux (coq-find-project-file))
-         (projectbuffer (and projectbuffer-aux (car projectbuffer-aux)))
-         (no-kill (and projectbuffer-aux (car (cdr projectbuffer-aux)))))
-    (if (not projectbuffer-aux)
-        (message "Coq project file not detected.")
-      (unless avoidargs (setq coq-prog-args (coq-search-prog-args projectbuffer)))
-      (unless avoidpath (setq coq-load-path (coq-search-load-path projectbuffer)))
-      (let ((msg
-             (cond
-              ((and avoidpath avoidargs) "Coqtop args and load path")
-              (avoidpath "Coqtop load path")
-              (avoidargs "Coqtop args")
-              (t ""))))
-        (message
-         "Coq project file detected: %s%s." (buffer-file-name projectbuffer)
-         (if (or avoidpath avoidargs)
-             (concat "\n(" msg " overridden by dir/file local values)")
-           "")))
-      (when coq-debug
-        (message "coq-prog-args: %S" coq-prog-args)
-        (message "coq-load-path: %S" coq-load-path))
-      (unless no-kill (kill-buffer projectbuffer)))))
-
-
-
-(defun coq-load-project-file ()
-  "Set `coq-prog-args' and `coq-load-path' according to _CoqProject file.
-Obeys `coq-use-project-file'. Note that if a variable is already
-set by dir/file local variables, this function will not override
-its value.
-See `coq-project-filename' to change the name of the
-project file, and `coq-use-project-file' to disable this
-feature."
-  (when coq-use-project-file
-    ;; Let us reread dir/file local vars, in case the user mmodified them
-    (let* ((oldargs (assoc 'coq-prog-args file-local-variables-alist))
-           (oldpath (assoc 'coq-load-path file-local-variables-alist)))
-      (coq-load-project-file-with-avoid oldargs oldpath))))
-
-
-(defun coq-load-project-file-rehack ()
-  "Reread file/dir local vars and call `coq-load-project-file'.
-Does nothing if `coq-use-project-file' is nil.
-Warning: 
-"
-  (when coq-use-project-file
-    ;; Let us reread dir/file local vars, in case the user mmodified them
-    (hack-local-variables)
-    ;; Useless since coq-load-project-file is in hack-local-variables-hook:
-    ;;(coq-load-project-file)
-    ))
-
-
-;; Since coq-project-filename can be set via .dir-locals.el or file variable,
-;; we need to call coq-load-coq-project-file only *after* local variables are
-;; set. But coq-mode-hook is called BEFORE local variables are read. Therefore
-;; coq-load-coq-project-file is added to hack-local-variables-hook instead. To
-;; avoid adding for other modes , the setting is performed inside
-;; coq-mode-hook. This is described in www.emacswiki.org/emacs/LocalVariables
-
-;; TODO: also read COQBIN somewhere?
-;; Note: this does not need to be at a particular place in the hook, but we
-;; need to make this hook local.
-;; hack-local-variables-hook seems to hack local and dir local vars.
-(add-hook 'coq-mode-hook
-          '(lambda ()
-             (add-hook 'hack-local-variables-hook
-                       'coq-load-project-file
-                       nil t)))
-
-;; smie's parenthesis blinking is too slow, let us have the default one back
-(add-hook 'coq-mode-hook
-          '(lambda ()
-             (when (and (fboundp 'show-paren--default)
-                        (boundp 'show-paren-data-function))
-               (setq show-paren-data-function 'show-paren--default))))
-
 
 
-(defun coq-toggle-use-project-file ()
-  (interactive)
-  (setq coq-use-project-file (not coq-use-project-file))
-  (when coq-use-project-file (coq-load-project-file-rehack))
-  ;; FIXME What should we do when disabling project file? since
-  ;; local variables override project file anyway, reading them
-  ;; again is useless. Let us do nothing.
-  ;;(setq coq-load-path nil)
-  ;;(setq coq-prog-args nil)
-  )
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -1601,23 +1298,6 @@ Warning:
     ))
 
 
-;
-;(defun coq-is-at-cmd-first-line-p ()
-;  (save-excursion
-;    (let ((l1 (line-number-at-pos)))
-;      (coq-find-real-start)
-;      (equal l1 (line-number-at-pos)))))
-;
-
-;
-;(defun coq-indent-command ()
-;  (save-excursion
-;    (when (coq-is-at-cmd-first-line-p)
-;      (let ((kind (coq-back-to-indentation-prevline)))
-;        (if 
-;        (current-column))))))
-;
-
 (defun coq-get-comment-region (pt)
   "Return a list of the forme (beg end) where beg,end is the comment region arount position PT.
 Return nil if PT is not inside a comment"
@@ -1968,10 +1648,11 @@ Near here means PT is either inside or just aside of a comment."
   :type 'integer
   :setting "Set Printing Depth %i . ")
 
-(defpacustom undo-depth coq-default-undo-limit
-  "Depth of undo history.  Undo behaviour will break beyond this size."
-  :type 'integer
-  :setting "Set Undo %i . ")
+;;; Obsolete:
+;;(defpacustom undo-depth coq-default-undo-limit
+;;  "Depth of undo history.  Undo behaviour will break beyond this size."
+;;  :type 'integer
+;;  :setting "Set Undo %i . ")
 
 (defun coq-set-search-blacklist (s)
   (let ((res (format "Remove Search Blacklist %s. \nAdd Search Blacklist %s. "