_CoqProject

-Q theories GhostTT

theories/Util.v

theories/BasicAST.v

theories/autosubst/core.v
theories/autosubst/unscoped.v
theories/autosubst/GAST.v
theories/autosubst/CCAST.v
theories/autosubst/RAsimpl.v
theories/autosubst/CCAST_rasimpl.v
theories/autosubst/GAST_rasimpl.v

theories/SubstNotations.v

theories/ContextDecl.v
theories/CastRemoval.v
theories/Scoping.v
theories/TermMode.v
theories/Univ.v
theories/TermNotations.v
theories/Typing.v
theories/BasicMetaTheory.v

theories/CScoping.v
theories/CTyping.v
theories/CCMetaTheory.v

theories/Erasure.v
theories/Revival.v
theories/Param.v

theories/Model.v
theories/Admissible.v

theories/FreeTheorem.v
theories/Examples.v

theories/RTyping.v
theories/Potential.v
theories/ElimReflection.v

theories/TransNat.v
theories/TransVec.v

theories/Assumptions.v