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").

• Redundant information added to speed-up elaboration:

  • Useless for browsing purposes
  • Possibly useless to other proof-checkers
  • Leads to problems of consistency: redundancy requires checks