Fixed a problem with a wrong side effect on syntax databases (when

sorting for menus).

1 files changed, 3 insertions, 2 deletions

diff --git a/coq/coq.el b/coq/coq.el
index b0c0e476..9f507412 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -86,6 +86,9 @@ To disable coqc being called (and use only make), set this to nil."
 ;; library `un-define' to work on xemacs."
 ;; (or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil))
 ;; da: I think the default t setting now works fine, at least for me.
+;; pc: 8.0 backward compliance:
+(if coq-version-is-V8-0 (setq proof-shell-unicode nil))
+
 
 (defcustom coq-prog-env nil
   "*List of environment settings d to pass to Coq process.
@@ -940,8 +943,6 @@ To be used in `proof-shell-process-output-system-specific'."
       )))
 
 
-
-
 (defun coq-shell-mode-config ()
   (setq 
    proof-shell-prompt-pattern coq-shell-prompt-pattern