Encoding CIC in XML: cooking and naming
In Coq it is possible to open a section, declare some variables, define objects depending on them and close the section
