Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in

coqdep since it is now deterministic (later -R's overwriting former ones).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13432 85f007b7-540e-0410-9357-904b9bb8a0f7

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 0000000000..6296941862
--- /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 0000000000..fc82069e5b
--- /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 0000000000..68b48d604e
--- /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 0000000000..b745fbd482
--- /dev/null
+++ b/test-suite/misc/deps/lib/foo.v
@@ -0,0 +1 @@
+Definition a := 0.