  Proof assistants like Coq are increasingly popular to help mathematicians
carry out proofs of the results they conjecture. However, formal proofs remain
highly technical and are especially difficult to reuse. In this paper, we
present a framework to carry out a posteriori script transformations. These
transformations are meant to be applied as an automated post-processing step,
once the proof has been completed. As an example, we present a transformation
which takes an arbitrary large proof script and produces an equivalent
single-line proof script, which can be executed by Coq in one single step.
Other applications, such as fully expanding a proof script (for debugging
purposes), removing all named hypotheses, etc. could be developed within this
framework. We apply our tool to various Coq proof scripts, including some from
the GeoCoq library.
