I took the following code from https://coq.inria.fr/library/Coq.Init.Datatypes.html:
Inductive prod (A B:Type) : Type :=
pair : A -> B -> A * B
where "x * y" := (prod x y) : type_scope.
Add Printing Let prod.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Section projections.
Context {A : Type} {B : Type}.
Definition fst (p:A * B) := match p with (x, y) => x end.
Definition snd (p:A * B) := match p with (x, y) => y end.
End projections.
When I load it into CoqIDE, at Definition fst... it comes up with the message The constructor pair (in type prod) expects 4 arguments.. How can I resolve this problem?