HoTT/HoTT — pull request #469 by mikeshulman (2014-09-07 23:53:40+00:00)
Title: 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.