Attempt to fix compile problems

3 files changed, 28 insertions, 23 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 78863d27..e79f361f 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -54,15 +54,16 @@
 
 ;;; The abbrev table built from keywords tables
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
-(if (and (boundp 'coq-mode-abbrev-table)
-	 (not (equal coq-mode-abbrev-table (make-abbrev-table)))) 
-    (message "Coq abbrevs already exists, default not loaded")    
-  (message "Coq default abbrevs loaded")
-  (define-abbrev-table 'coq-mode-abbrev-table
-    (append coq-tactics-abbrev-table coq-tacticals-abbrev-table 
-	    coq-commands-abbrev-table coq-terms-abbrev-table))
-  ;if we use default coq abbrev, never ask to save it
-  (setq save-abbrevs nil))
+(eval-when (load)
+  (if (and (boundp 'coq-mode-abbrev-table)
+	   (not (equal coq-mode-abbrev-table (make-abbrev-table)))) 
+      (message "Coq abbrevs already exists, default not loaded")    
+    (message "Coq default abbrevs loaded")
+    (define-abbrev-table 'coq-mode-abbrev-table
+      (append coq-tactics-abbrev-table coq-tacticals-abbrev-table 
+	      coq-commands-abbrev-table coq-terms-abbrev-table))
+    ;; if we use default coq abbrev, never ask to save it
+    (setq save-abbrevs nil)))
 
 ;;;;;
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index dfda8ee7..87f587a1 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -9,14 +9,23 @@
 (require 'proof-syntax)
 (require 'coq-db)
 
-;; da 15/2/03: without defvars compilation breaks
-;; This may have broken some of logic below
+(defcustom coq-prog-name   ;; da: moved from coq.el since needed here
+    "coqtop"
+;; On Windows with latest Coq package you might need something like:
+;;  "C:/Program Files/Coq/bin/coqtop.opt.exe"
+;; instead of just "coqtop".  See also coq-prog-env below.
+  "*Name of program to run as Coq. Important: See `proof-prog-name'."
+  :type 'string
+  :group 'coq)
 
 ;; Pierre: we will have both versions V8.0 and V8.1 during a while the
 ;; test with "coqtop -v" can be skipped if one of the variables
 ;; coq-version-is-V8-0/1 is already set (useful for people dealing
 ;; with several version of coq).
 
+;; DA: please ensure this file compiles!  top-level forms need to be delayed
+;; during compile explicitly so they are evaluated during load.
+
 ; this one is temporary, for compatibility
 (defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.")
 
@@ -36,8 +45,9 @@ coq-version-is-V8-0. If none of these 2 variables is set to t, then
 ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
 
 
-;; post-cond: one of the variables is set to t
-(eval-when (load)
+(defun coq-determine-version ()
+  "Intuit the version of Coq we're using and configure accordingly."
+  ;; post-cond: one of the variables is set to t
   (let* 
       (
        (seedoc (concat " (to force another version, see for example"
@@ -73,6 +83,9 @@ ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
             (message (concat "Falling back to default: " v81))
             (setq coq-version-is-V8-1 t)))))))))
 
+(eval-when (load)
+  (coq-determine-version))
+
 
 ;;; keyword databases
 
@@ -744,7 +757,7 @@ Used by `coq-goal-command-p'"
  (cond 
   (coq-version-is-V8-1 (coq-goal-command-str-v81-p str))
   (coq-version-is-V8-0 (coq-goal-command-str-v80-p str))
-  (t (coq-goal-command-p-str-v80-p str)) ;; this is temporary
+  (t (coq-goal-command-str-v80-p str)) ;; this is temporary
   ))
 
 ;; This is used for backtracking
diff --git a/coq/coq.el b/coq/coq.el
index 78915803..799404ff 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -25,15 +25,6 @@
 ;; (defun proofstack () (coq-get-span-proofstack (span-at (point) 'type)))
 ;; End debugging
 
-(defcustom coq-prog-name 
-    "coqtop"
-;; On Windows with latest Coq package you might need something like:
-;;  "C:/Program Files/Coq/bin/coqtop.opt.exe"
-;; instead of just "coqtop".  See also coq-prog-env below.
-  "*Name of program to run as Coq. Important: See `proof-prog-name'."
-  :type 'string
-  :group 'coq)
-
 ;; List of arguments to pass to Coq process.  Should contain -emacs.
 ;; -translate will be added automatically to this list if `coq-translate-to-v8'
 ;; is set.