aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5043.v
blob: 4e6a0f878f73cdce45a0d4a8f6c0b5c66a1c436b (plain)
1
2
3
4
5
6
7
8
Unset Keep Admitted Variables.

Section a.
  Context (x : Type).
  Definition foo : Type.
  Admitted.
End a.
Check foo : Type.