1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
|
(* Check BZ#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.
(* Check BZ#2809: correct printing of modules with notations *)
Module C.
Inductive test : Type :=
| c1 : test
| c2 : nat -> test.
Notation "! x" := (c2 x) (at level 50).
End C.
Print C. (* Should print test_rect without failing *)
|