test-suite/bugs/closed/3355.v


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.