(* 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 := 9.


(* This is line 31 *)
Lemma x : b + c + k = sum.
Proof using.
  unfold b, c, k, sum in *.
  simpl.
  trivial.
Qed.
(* This is line 38 *)