aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/multiple-files-multiple-dir/README
diff options
context:
space:
mode:
Diffstat (limited to 'coq/ex/test-cases/multiple-files-multiple-dir/README')
-rw-r--r--coq/ex/test-cases/multiple-files-multiple-dir/README23
1 files changed, 23 insertions, 0 deletions
diff --git a/coq/ex/test-cases/multiple-files-multiple-dir/README b/coq/ex/test-cases/multiple-files-multiple-dir/README
new file mode 100644
index 00000000..82c7fc2a
--- /dev/null
+++ b/coq/ex/test-cases/multiple-files-multiple-dir/README
@@ -0,0 +1,23 @@
+Test multiple file support when files are distributed over
+different directories.
+
+Dependency graph
+
+ a/a.v
+ \
+ \
+ b/b1.v --- b/b2.v
+ \
+ \
+ c/c.v
+
+That is, c depends on b2, which depends on b1, which depends on
+a.
+
+Script c.v and watch the compilation messages in *Messages*.
+Touch any file and retract and assert the Require in c.
+
+The bugs described in ../multiple-files-single-dir/README can
+also be reproduced here.
+
+