Don't use "Set Implicit Arguments" in the core.

I am aware that this may be controversial, so feel free to object.  But personally, I dislike "Set Implicit Arguments" a lot; it annoys me to no end when I read a function definition and realize that I can't tell by looking at it which arguments are implicit; I have to compile it and ask Coq.  It's also not clear to me that Coq always makes the "right" choice anyway.