diff options
| author | Hendrik Tews | 2021-01-01 22:56:48 +0100 |
|---|---|---|
| committer | hendriktews | 2021-01-10 20:59:43 +0100 |
| commit | 0d731606bee81b2d73895a23b69e84796ea7e4e7 (patch) | |
| tree | 2df103ffc973c9728a866d27ab3ea325f178658e /ci/compile-tests/007-slow-require/c4.v.orig | |
| parent | 2d94aa0aabf0aa7087f8833e1c61d95a034e2d13 (diff) | |
add Coq compile test for a delayed require
Diffstat (limited to 'ci/compile-tests/007-slow-require/c4.v.orig')
| -rw-r--r-- | ci/compile-tests/007-slow-require/c4.v.orig | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/ci/compile-tests/007-slow-require/c4.v.orig b/ci/compile-tests/007-slow-require/c4.v.orig new file mode 100644 index 00000000..400a8a6c --- /dev/null +++ b/ci/compile-tests/007-slow-require/c4.v.orig @@ -0,0 +1,27 @@ +(* This file is part of Proof General. + * + * © Copyright 2021 Hendrik Tews + * + * Authors: Hendrik Tews + * Maintainer: Hendrik Tews <hendrik@askra.de> + * + * License: GPL (GNU GENERAL PUBLIC LICENSE) + * + * + * This file is part of an automatic test case for parallel background + * compilation in coq-par-compile.el. See test.el in this directory. + *) + +(* The test script relies on absolute line numbers. + * DO NOT INSERT ANY LINE UNLESS YOU KNOW WHAT YOU ARE DOING. + *) + +(* Specify delays for coqdep and coqc when processing this file: + * coqdep-delay 0 + * coqc-delay 0 + *) + +Require Export d4. + +(* This is line 26 *) +Definition c : nat := 3. |