coq/ex/test-cases/require-string/b.v


1
2
3
4
5
6
7
8

(* This file depends on a.v. *)

(* The following works in Proof General 4.0, if a.v has been compiled and
 * if the path is the correct absolute path.
 *)
Require "/home/tews/src/pg/coq/ex/test-cases/require-string/a".

Print a.a.