Through the Curry-Howard correspondence, dependent type theories are appealing to both the mathematical and the programming community. To the first, they provide an expressive logical framework, in which mathematics can be developed. To the second, they offer a functional programming language that allows to state precise invariants programs have to respect and to build certified proofs thereof. Several dependent type systems have been investigated and implemented, with some early ones geared more to-wards the mathematical community [Con+86; Pol94; Coq12], called proof-assistants, and later putting a stronger accent on their viability as a programming environment [McB99; Nor07; Soz08]. The Calculus of Inductive Constructions (pCIC) is one such theory that attempts to stay faithful to the correspondence and bridge the two worlds of programming and proving. It is implemented in the Coq system [Coq12] and Matita [Asp+11]. The utilisation of Coq as a programming language as advocated by Sozeau relies on extending pCIC with a principle known as proof-irrelevance, which means that any two proofs of a logical proposition are identified by the system. This principle does not hold in the current theory and implementation of Coq , but as proofs appear as parts of dependently typed programs, they get in the way during their verification. Furthermore, it corresponds to the mathematical intuition that the existence of a proof of a theorem is more important than its exact wording. In fact, under this aspect, there have been demands for proof-irrelevance in the community of interactive theorem provers since the beginning of their development, for instance in automath [Ned94, Sec. D.3]. We studied how to extend pCIC in order to incorporate this principle.