aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3355.v
blob: 46a57147813d13230b3393a4ef184e0977fe1311 (plain)
1
2
3
4
5
6
Inductive paths {A} (x : A) : A -> Type := idpath : paths x x.
Goal forall A B : Set, @paths Type A B -> @paths Set A B.
Proof.
  intros A B H.
  Fail exact H.
Abort.