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

• Once a section is closed, cooking starts: all the variables are got rid of, the objects are parametrized w.r.t. them and their Section Path is changed. This is an example

• Objects are identified by their name and not by their Section Path ===> it is not possible to declare two objects that, once cooked, has the same name