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 | |
| parent | c5384ee0ce6232fa89c07864e60be70dee2ad7ed (diff) | |
coq-goal-command-str-p: Fix suspected typo shown up by compile warning.
| -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 |