diff options
| -rw-r--r-- | test-suite/bugs/closed/4078.v | 14 |
1 files changed, 14 insertions, 0 deletions
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. |