test-suite/bugs/closed/bug_4603.v


1
2
3
4
5
6
7
8
9
10

Axiom A : Type.

Goal True. exact I.
Check (fun P => P A).
Abort.

Goal True.
Definition foo (A : Type) : Prop:= True.
  set (x:=foo). split.
Qed.