diff options
| -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")))) |