From 1f8b780b72b36b9ca4605453b9fe73bbc9dd4c23 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 14 Dec 2007 01:22:59 +0000 Subject: Improve loading; these tests are not functioning yet --- coq/coq-autotest.el | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'coq/coq-autotest.el') 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)) -- cgit v1.2.3