Document language interface
It would be good to document the language interfaces of Iris and how to instantiate Iris with one's own language, define one's own wp_ tactics, and so on.
Considering #131 (closed), it may be good to have a separate folder with Coq related documentation, also including the current ProofMode.md. We could also LaTeX-ify all Coq documentation, and add it to the already existing theoretical documentation.