aboutsummaryrefslogtreecommitdiff
path: root/ci/compile-tests/007-slow-require/d1.v.orig
blob: fec9578782f6259b57610539cf0eed239815c027 (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
26
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.