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.