blob: 1286905209ef53e59a79a8fd555b48ac05b25895 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
;; coq-autotest.el: tests of Coq Proof General (in progress).
;;
;; You can run these by issuing "make test.coq" in PG home dir.
;;
;; $Id$
;;
(eval-when-compile
(require 'cl))
(eval-when (compile)
(require 'proof-site)
(proof-ready-for-assistant 'coq))
(require 'pg-autotest)
;; The included test files
(unless noninteractive
(pg-autotest remark "Testing standard examples...")
(pg-autotest script-wholefile "coq/example.v")
(pg-autotest script-wholefile "coq/example-tokens.v")
(pg-autotest script-wholefile "coq/ex-module.v")
(pg-autotest quit-prover)
(pg-autotest exit))
|
