Pair definition in Coq has type "(Set * Set)%type" while it is expected to have type "Type"

Question

I am reading Software Foundations(*) and have an issue with defining types in Coq: In the example below I tried to make 2 type definitions. t1 is the list of naturals, and t2 is a pair of naturals.

The first definition t1 is accepted by Coq but definition t2 is rejected with the error message:

The term (nat, nat) has type (Set * Set)%type while it is expected to have type Type.

I don't quite understand what is wrong and what this message means. What is wrong with definition t2?

  Definition t1 : Type := list nat.
  Definition t2 : Type := pair nat nat.

(*) http://www.cis.upenn.edu/~bcpierce/sf/Lists.html#lab58

Answer 1

No, pair is the constructor, prod is the type.

Print prod.
Check prod.
Check @pair.

Definition t1 : Type := list nat.
Definition t2 : Type := prod nat nat.
Definition t2' : Type := (nat * nat)%type.