blob: f3d28e82ab2bc61d412009776d3a97f7558ee188 (
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
28
29
30
31
32
33
34
35
36
37
38
|
(* This file is part of Proof General.
*
* © Copyright 2020 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.
*)
(* This is line 21 *)
Require Export b.
Require Export c.
(* This is line 24 *)
(* This is line 27 *)
Definition sum : nat := 35.
(* This is line 31 *)
Lemma x : b + c + d + e + f + g + h = sum.
Proof using.
unfold b, c, d, e, f, g, h, sum in *.
simpl.
trivial.
Qed.
(* This is line 38 *)
|
