diff options
Diffstat (limited to 'ci/compile-tests/007-slow-require/a5.v.orig')
| -rw-r--r-- | ci/compile-tests/007-slow-require/a5.v.orig | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/ci/compile-tests/007-slow-require/a5.v.orig b/ci/compile-tests/007-slow-require/a5.v.orig new file mode 100644 index 00000000..b6d7edbb --- /dev/null +++ b/ci/compile-tests/007-slow-require/a5.v.orig @@ -0,0 +1,41 @@ +(* 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. + *) + +(* The delay for coqdep is specified in comments with key coqdep-delay, + * see compile-test-start-delayed. + *) + + +(* This is line 24 *) +Require Export b5. +Require Export c5. +(* This is line 27 *) + + +(* This is line 30 *) +Definition sum : nat := 9. + + +(* This is line 34 *) +Lemma x : b + c + d = sum. +Proof using. + unfold b, c, d, sum in *. + simpl. + trivial. +Qed. +(* This is line 41 *) |