aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/multiple-files-multiple-dir/README
blob: 82c7fc2a046dcb4541956a046374fcfb27d54cfe (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
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.