I think it's useful for not having to write everything all the time, and letting Coq figure out what's automatically inferrable, but I recognize that it's yet another thing that could confuse a beginner.  I've removed it (but I don't plan to remove it from, e.g., the category theory code, unless there's a strong argument to).