From b3a76a8ea645f90123fbde1db42b305edd4baa9d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 1 Sep 2009 22:02:01 +0000
Subject: Remove some old X-Symbol references.

---
 coq/coq-autotest.el | 2 +-
 coq/coq-indent.el   | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index a179a596..35e21030 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -11,7 +11,7 @@
 (unless noninteractive
   (pg-autotest  message "Testing standard examples")
   (pg-autotest script-wholefile "coq/example.v")
-  (pg-autotest script-wholefile "coq/example-x-symbol.v")
+  (pg-autotest script-wholefile "coq/example-tokens.v")
   (pg-autotest script-wholefile "coq/ex-module.v")
 
   (pg-autotest-quit-prover)
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 3258ebe3..d16b635a 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -20,9 +20,8 @@
 (defconst coq-indent-inner-regexp
   (proof-regexp-alt
    "[[]()]" "|" "šÕ"
-   ;; forall with x-symbol (nomule) must not be enclosed by \\<and
-   ;;\\> . "~" forall x-symb mule but interacts
-   ;;with 'not'
+   ;; forall with must not be enclosed by \\< and
+   ;;\\> . "~" forall but interacts with 'not'
    (proof-ids-to-regexp
     '("as" "Cases" "match" "else" "Fix" "forall" "fun" "if" "into" "let" "then"
       "using" "after"))))
-- 
cgit v1.2.3