5043.v « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

path: root/test-suite/bugs/closed/5043.v

blob: 4e6a0f878f73cdce45a0d4a8f6c0b5c66a1c436b (plain)

Unset Keep Admitted Variables.

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