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
Objects are exported before cooking ===> we must export
also the list of necessary ingredients (but this information is not
available inside Coq)
We identify objects by URIs that
correspond to their section path. E.g.:
"cic:/coq/INIT/Datatypes/nat.ind"