aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4653.v
blob: 4514342c5e1f1da1e1d91857325d9cf65f174b3a (plain)
1
2
3
Definition T := Type.
Module Type S. Parameter foo : let A := T in True. End S.
Module M <: S. Lemma foo (A := T) : True. Proof I. End M.