diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2006-05-26 14:15:30 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2006-05-26 14:15:30 +0000 |
| commit | 9d345c9ac435bf79541dd0cc3634375af9f7ece3 (patch) | |
| tree | 008523cd306ac7e25556db3d874fa9fe9b0b75f8 | |
| parent | 2991d4ee7958cbdf3b69f0a896b1ae5a454e1349 (diff) | |
Fix to work with coq 8.1 again (havent tested 8.0)
| -rw-r--r-- | coq/coq-syntax.el | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 349f5b86..10ff1816 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -208,7 +208,7 @@ Used by `coq-goal-command-p'" ;; TODO: have something in the prompt telling the name of all opened ;; modules (like for open goals), and use it to set goalcmd --> no more -;; need to look at "Modules" --> no more need to coq-goal-command-str-v81-p +;; need to look at "Modules" --> no more need to coq-goal-command-v80str-v81-p (defun coq-goal-command-p-v81 (span) "see `coq-goal-command-p'" (or (span-property span 'goalcmd) @@ -220,8 +220,8 @@ Used by `coq-goal-command-p'" "Decide whether argument is a goal or not." (cond (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-p-v80 span)) - (t (coq-goal-command-p-v80 span)) ;; this is temporary + (coq-version-is-V8-0 (coq-goal-command-p-v80 (span-property span 'cmd))) + (t (coq-goal-command-p-v80 (span-property span 'cmd))) ;; this is temporary )) (defvar coq-keywords-save-strict |