docgen should elide proof of lemmas (or make this an option) #949
Description
When docgen is turning an EasyCrypt file into .html, it seems to me that proofs of lemmas should be elided. The reader of the html wants to know what facilities are provided by the theory, and can look at the actual source to see the proofs.
It would also be great to have a way of telling docgen to ignore parts of a file. These might contain internal lemmas, etc., that a general user would find confusing. At the moment, these clutter up the output.