1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 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.