-R . Lambda
OTHERFLAGS = "-dump-glob globals.dump"
Utils.v
Tactics.v
MyList.v
ListType.v
Terms.v
LiftSubst.v
InvLiftSubst.v
Reduction.v
Conv.v
Conv_Dec.v
Env.v
# CCSum
CCSum/Types.v
CCSum/Thinning.v
CCSum/Substitution.v
CCSum/Inversion.v
CCSum/TypeCase.v
CCSum/SubjectReduction.v
CCSum/Unicity.v
# Russell
Russell/Types.v
Russell/Coercion.v
Russell/Inversion.v
Russell/Thinning.v
Russell/Substitution.v
Russell/GenerationNotKind.v
Russell/GenerationCoerce.v
Russell/Generation.v
Russell/GenerationRange.v
Russell/UnicityOfSortingRange.v
Russell/UnicityOfSorting.v
Russell/Injectivity.v
Russell/Depth.v
Russell/Narrowing.v
Russell/Transitivity.v
Russell/Inversion.v
Russell/SubjectReduction.v
Russell/Unicity.v
# JRussell
JRussell/Types.v
JRussell/Freevars.v
JRussell/Basic.v
JRussell/Conversion.v
JRussell/Coercion.v
JRussell/Thinning.v
JRussell/Substitution.v
JRussell/PreFunctionality.v
JRussell/Generation.v
JRussell/Validity.v
JRussell/GenerationNotKind.v
JRussell/GenerationCoerce.v
JRussell/GenerationRange.v
JRussell/UnicityOfSortingRange.v
JRussell/UnicityOfSorting.v
# TPOSR
TPOSR/Terms.v
TPOSR/LiftSubst.v
TPOSR/Reduction.v
TPOSR/Conv.v
TPOSR/Conv_Dec.v
TPOSR/Env.v
TPOSR/Unlab.v
TPOSR/Types.v
TPOSR/Basic.v
TPOSR/UnicityOfSorting.v
TPOSR/MaxLemmas.v
TPOSR/TypesDepth.v
TPOSR/Thinning.v
TPOSR/CtxReduction.v
TPOSR/CtxExpansion.v
TPOSR/LeftReflexivity.v
TPOSR/Substitution.v
TPOSR/PreSubstitutionTPOSR.v
TPOSR/PreCtxCoercion.v
TPOSR/RightReflexivity.v
TPOSR/CtxConversion.v
TPOSR/CtxCoercion.v
TPOSR/SubstitutionTPOSR.v
TPOSR/Equiv.v
TPOSR/Generation.v
TPOSR/Validity.v
TPOSR/TypesFunctionality.v
TPOSR/UniquenessOfTypes.v
TPOSR/ChurchRosserDepth.v
TPOSR/ChurchRosser.v
TPOSR/CoerceDepth.v
TPOSR/CoerceNoTrans.v
TPOSR/TransitivitySet.v
TPOSR/Transitivity.v
TPOSR/Injectivity.v
TPOSR/SubjectReduction.v
TPOSR/TPOSR_trans.v
TPOSR/UnlabConv.v
# Meta
Meta/JRussell_Russell.v
Meta/TPOSR_JRussell.v
Meta/TPOSR_Russell.v
Meta/Russell_TPOSR.v
Meta/Russell_JRussell.v
Meta/SubjectReduction.v
# Russell.
Russell./Types.v