From c43eebc79e84402f3978f1f32d812e755039e3ef Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 13 Feb 2005 21:36:23 +0000
Subject: Added simple testing framework (in progress)

---
 coq/coq-autotest.el | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 coq/coq-autotest.el

(limited to 'coq')

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
new file mode 100644
index 00000000..6d268b3d
--- /dev/null
+++ b/coq/coq-autotest.el
@@ -0,0 +1,19 @@
+;; coq-autotest.el: tests of Isar Proof General.
+;;
+;; You can run these by issuing "make devel.test.isar" in PG home dir.
+;;
+;; $Id$
+;;
+
+(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")
+
+(pg-autotest-quit-prover)
+(pg-autotest-finished)
+
+
-- 
cgit v1.2.3