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

• Tactis used for proving/defining: they are proof engine dependent. Moreover, they are not the real informative content and are not at the level at which a proof must be understood (example: "Auto" means not "Obvious").