aboutsummaryrefslogtreecommitdiff
path: root/ci/compile-tests/003-require-error/b.v
blob: e3f5da5fa30bcf876d77f9125c34129660644a26 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(* 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.
 *)

Definition b : nat := 2.