diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 01:22:59 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-14 01:22:59 +0000 |
| commit | 1f8b780b72b36b9ca4605453b9fe73bbc9dd4c23 (patch) | |
| tree | 9bae546af0e8a4804246121c99525b2b81ea315d /coq/coq-autotest.el | |
| parent | 8fa863dea38eb6471bc99f05328b53430fd78f8d (diff) | |
Improve loading; these tests are not functioning yet
Diffstat (limited to 'coq/coq-autotest.el')
| -rw-r--r-- | coq/coq-autotest.el | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 6d268b3d..0e12d48c 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -1,6 +1,6 @@ -;; coq-autotest.el: tests of Isar Proof General. +;; coq-autotest.el: tests of Coq Proof General (in progress). ;; -;; You can run these by issuing "make devel.test.isar" in PG home dir. +;; You can run these by issuing "make test.coq" in PG home dir. ;; ;; $Id$ ;; @@ -8,12 +8,13 @@ (require 'pg-autotest) ;; The included test files -(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/ex-module.v") +(eval-when (load) + (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/ex-module.v") -(pg-autotest-quit-prover) -(pg-autotest-finished) + (pg-autotest-quit-prover) + (pg-autotest-finished)) |