aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/require-string/b.v
diff options
context:
space:
mode:
Diffstat (limited to 'coq/ex/test-cases/require-string/b.v')
-rw-r--r--coq/ex/test-cases/require-string/b.v8
1 files changed, 8 insertions, 0 deletions
diff --git a/coq/ex/test-cases/require-string/b.v b/coq/ex/test-cases/require-string/b.v
new file mode 100644
index 00000000..219c29e2
--- /dev/null
+++ b/coq/ex/test-cases/require-string/b.v
@@ -0,0 +1,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. \ No newline at end of file