diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 00:59:31 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 00:59:31 +0000 |
commit | 0af55a781ea033085a3149cafc7942dd6a2f2290 (patch) | |
tree | 304d8e9498a83d6daf9de98077481ba43e22aa2f /coq/coq-syntax.el | |
parent | c5384ee0ce6232fa89c07864e60be70dee2ad7ed (diff) |
coq-goal-command-str-p: Fix suspected typo shown up by compile warning.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r-- | coq/coq-syntax.el | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index ab0fd279..dfda8ee7 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -36,10 +36,8 @@ 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'." ) - -;;FIXME: how to make compilable? ;; post-cond: one of the variables is set to t -(unless (noninteractive);; DA: evaluating here gives error during compile +(eval-when (load) (let* ( (seedoc (concat " (to force another version, see for example" @@ -746,7 +744,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 str)) ;; this is temporary + (t (coq-goal-command-p-str-v80-p str)) ;; this is temporary )) ;; This is used for backtracking |