Encoding CIC in XML: theories

• In Coq, a section is an ordered list of objects or (sub)section declarations and is used not only to structure a ".v" file, but also to delimit (in questionable ways!) the scope of objects declarations. Moreover, inside a section, another one could be required with the effect of importing all the declarations which are not out of scope