implicit arguments in quotient.v, close #447

My standard is "anything that helps explain the current state of the code should go in the coqdoc documentation, private notes like todo lists should not".  And `(* The path constructors. *)` seems to be of general interest.  But these are not terribly important.