prev slide

prev

contents

next

next slide

Encoding CIC in XML:

what must NOT be exported from Coq

Parsing rules: proof-engine dependent