Encoding CIC in XML: terms and objects
In CIC we have (lambda)terms, objects, sections.
Lambda terms never occur alone (would have no meaning),
but only inside objects ===> markup for terms will be nested inside markup
for objects
Objects, instead, are autonomous entities, completely
identified in Coq by a name and a Section Path ===> every object is
exported to a file whose name is the name of the object. The files
are structured in directories, one for each Coq section, so that the
path of the XML file becomes the Section Path of the Coq object