We study formal proofs conceived to be checked automatically. These proofs arerarely used. We think that it is partly due to the fact that it is very difficult for ahuman to understand the connection between what he considers a mathematicalproof and its formal representation. We are interested in automatically producingtext explaining these formal representations. We have chosen to produce text innatural language using the traditional vocabulary of mathematics.More precisely, we work on a formalism called Calculus ofInductiveConstructions, which uses a functional representation of proofs.The objective ofthis formalism is to allow an automatic proof checking by a simple machine.Each aspect, simplicity and automation, imposes its own specificity tothe proofrepresentation. On the one hand, the proofs contain a lot of trivialities that wouldbe considered useless by human readers. On the other hand, some informationthat would be very useful to these same human readers are omitted.In previous work [3], we have developed a machine that translatesproofs ofthe Calculus of Inductive Constructions into natural language.The textproduced by this machine has the same structure as the formal proof. These textsare not satisfactory. They are in general too verbose, and sometimes they omitimportant information. In this article, we will present an improvement of thistranslation based on a more precise choice of the information we include in thetext.