In Coq, "if then else" allows non-boolean first argument?

I read in a few tutorials that if a then b else c stands for match a with true => b | false => c end. However the former very strangely does not check the type of a, while the latter of course makes sure that a is a boolean. For instance,

Coq < Check if nil then 1 else 2.
if nil then 1 else 2
     : nat
where
?A : [ |- Type] 


Coq < Check match nil with true => 1 | false => 2 end.
Toplevel input, characters 33-38:
> Check match nil with true => 1 | false => 2 end.
>                                  ^^^^^
Error: Found a constructor of inductive type bool while
a constructor of list is expected.

Why is if ... then ... else ... allowing its first argument to be anything else than a non-boolean? Is there some overloading going on? (Locate "if". gives no result.)