(* 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.