Encoding CIC in XML:

what must NOT be exported from Coq

• Parsing rules: proof-engine dependent

• Pretty-printing rules: should depend only on the author and user choices and on the available browser