blob: 9ad3779d16c22a22dac87c06a1fda8e2098c1b8f (
plain)
1
2
3
4
5
6
7
8
|
Set Primitive Projections.
Record prod A B := pair { fst : A; snd : B}.
Goal fst (@pair Type Type Type Type).
Set Printing All.
Fail match goal with |- ?f _ => idtac end.
(* Toplevel input, characters 7-44:
Error: No matching clauses for match. *)
|
