  Due to their numerous advantages, formal proofs and proof assistants, such as
Coq, are becoming increasingly popular. However, one disadvantage of using
proof assistants is that the resulting proofs can sometimes be hard to read and
understand, particularly for less-experienced users. To address this issue, we
have implemented a tool capable of generating natural language versions of Coq
proofs called Coqatoo, which we present in this paper.
