Dependent Type Theory as implemented into proof assistants and programming languages like Coq and Agda provide a firm and general basis for the formalization of mathematics and computer software. However, the core dependent type theory exposes a rather spartan interface for programming and writing proofs. Over the years a number of higher-level constructs and techniques have been developed to overcome this difficulty without touching the core language. For instance, implicit syntax, tactics and meta-languages like Ltac have been used successfully to make systems more accessible, automatable and scalable. Our research investigates further elaborations from high-level languages into dependent type theory. We present three such elaborations that facilitate programming with proofs, inductive families and overloaded functions in the Coq proof assistant. We demonstrate their usefulness for defining objects and structuring developments, as well as their crucial help in proofs.