aboutsummaryrefslogtreecommitdiff
path: root/ci/compile-tests/007-slow-require/d2.v.orig
diff options
context:
space:
mode:
Diffstat (limited to 'ci/compile-tests/007-slow-require/d2.v.orig')
-rw-r--r--ci/compile-tests/007-slow-require/d2.v.orig27
1 files changed, 27 insertions, 0 deletions
diff --git a/ci/compile-tests/007-slow-require/d2.v.orig b/ci/compile-tests/007-slow-require/d2.v.orig
new file mode 100644
index 00000000..fec95787
--- /dev/null
+++ b/ci/compile-tests/007-slow-require/d2.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
+ *)
+
+
+
+(* This is line 26 *)
+Definition d : nat := 4.