diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2009-09-01 22:02:01 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-01 22:02:01 +0000 |
commit | b3a76a8ea645f90123fbde1db42b305edd4baa9d (patch) | |
tree | cc27678a5e6f1a66600eaa516f9e022e167af22b | |
parent | 7260cde3d4041ef3d8d72ba82e6873a8ae247d40 (diff) |
Remove some old X-Symbol references.
-rw-r--r-- | coq/coq-autotest.el | 2 | ||||
-rw-r--r-- | 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")))) |