aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/add-load-path-unsupported/b/b.v
diff options
context:
space:
mode:
Diffstat (limited to 'coq/ex/test-cases/add-load-path-unsupported/b/b.v')
-rw-r--r--coq/ex/test-cases/add-load-path-unsupported/b/b.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/coq/ex/test-cases/add-load-path-unsupported/b/b.v b/coq/ex/test-cases/add-load-path-unsupported/b/b.v
new file mode 100644
index 00000000..226b71ee
--- /dev/null
+++ b/coq/ex/test-cases/add-load-path-unsupported/b/b.v
@@ -0,0 +1,7 @@
+(* This file depends on ../a/a.v *)
+
+Add LoadPath "../a".
+
+Require a.
+
+Print a.a. \ No newline at end of file