3043.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: 12885987f813a7ead73de8e5e091449258a74056 (plain)

1
2
3

Goal (fun A (P : A -> Prop) (X : sigT P) => proj1_sig X) = (fun A (P : A -> Prop) (X : sigT P) => projT1 X).
  reflexivity.
Qed.