diff options
Diffstat (limited to 'test-suite/success/Mod_type.v')
-rw-r--r-- | test-suite/success/Mod_type.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v new file mode 100644 index 00000000..b847833f --- /dev/null +++ b/test-suite/success/Mod_type.v @@ -0,0 +1,19 @@ +(* Check bug #1025 submitted by Pierre-Luc Carmel Biron *) + +Module Type FOO. + Parameter A : Type. +End FOO. + +Module Type BAR. + Declare Module Foo : FOO. +End BAR. + +Module Bar : BAR. + + Module Fu : FOO. + Definition A := Prop. + End Fu. + + Module Foo := Fu. + +End Bar. |