(* This file is part of Proof General. * * © Copyright 2020 Hendrik Tews * * Authors: Hendrik Tews * Maintainer: Hendrik Tews * * 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 Coq.Bool.Bool. Definition a : nat := 0. (* This is line 24 *)