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.
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).