test-suite/bugs/closed/bug_12930.v


1
2
3
4
5
6
7
8
9
10

Section S.
  Variable v : Prop.
  Variable vv : v.
  Collection easy := Type*.

  Lemma ybar : v.
  Proof using easy.
    exact vv.
  Qed.
End S.