Matches on integers don't work in coq

[Nadrieril]

trafficstars

Example:

fn match_u32(x: u32) -> u32 {
    match x {
        0 => 0,
        1 => 1,
        _ => 2,
    }
}

gives:

Definition match_u32 (x : u32) : result u32 :=
  match x with | 0%u32 => Ok 0%u32 | 1%u32 => Ok 1%u32 | _ => Ok 2%u32 end
.