aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq-autotest.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq-autotest.el')
-rw-r--r--coq/coq-autotest.el19
1 files changed, 19 insertions, 0 deletions
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)
+
+