A LaTeX comment is started by (*! doc1 doc2 ... (on the same line)
and ended by *). As far as building the proof is concerned, these
comments are ignored. doc1, doc2, ... must be among the document
names declared in the header. Thus, when compiling a file, the content
of these comments are directly outputed to the corresponding LaTeX files
(except for the formulas as we will see in the next section).