From cab07133acbce19e865b8302fef24dd4ea190d90 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 21 Feb 2015 19:19:55 +0100
Subject: Test for bug #4078.

---
 test-suite/bugs/closed/4078.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/bugs/closed/4078.v

diff --git a/test-suite/bugs/closed/4078.v b/test-suite/bugs/closed/4078.v
new file mode 100644
index 0000000000..236cd2fbb1
--- /dev/null
+++ b/test-suite/bugs/closed/4078.v
@@ -0,0 +1,14 @@
+Module Type S.
+
+Axiom foo : nat.
+
+End S.
+
+Module M : S.
+
+Definition bar := 0.
+Definition foo := bar.
+
+End M.
+
+Print All Dependencies M.foo.
-- 
cgit v1.2.3