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
A theory should be a (structured) mathematical
document composed using objects taken almost freely from different
sections.
Writing a new theory means developing new
objects and assembling these and older ones into the theory.
In Coq theories do not exist. The closest idea
is the one of ".v" files which are thought as root sections.
From each ".v". file we generate a corresponding
XML theory file, substituting object definitions with references to them.