Imported Upstream version 8.3upstream/8.3

4 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/misc/deps/client/bar.v b/test-suite/misc/deps/client/bar.v
new file mode 100644
index 00000000..62969418
--- /dev/null
+++ b/test-suite/misc/deps/client/bar.v
@@ -0,0 +1,11 @@
+(* We assume the file compiled with -R ../lib lib -R . client *)
+(* foo alone should refer to client.foo because -R . client comes last *)
+
+Require Import foo.
+Goal a = 1.
+reflexivity.
+Qed.
+Require Import lib.foo.
+Goal a = 0.
+reflexivity.
+Qed.
diff --git a/test-suite/misc/deps/client/foo.v b/test-suite/misc/deps/client/foo.v
new file mode 100644
index 00000000..fc82069e
--- /dev/null
+++ b/test-suite/misc/deps/client/foo.v
@@ -0,0 +1 @@
+Definition a := 1.
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
new file mode 100644
index 00000000..68b48d60
--- /dev/null
+++ b/test-suite/misc/deps/deps.out
@@ -0,0 +1 @@
+misc/deps/client/bar.vo misc/deps/client/bar.glob: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/misc/deps/lib/foo.v b/test-suite/misc/deps/lib/foo.v
new file mode 100644
index 00000000..b745fbd4
--- /dev/null
+++ b/test-suite/misc/deps/lib/foo.v
@@ -0,0 +1 @@
+Definition a := 0.