_CoqProject

-arg "-w -parsing"
-R . DiffTraces

MyNotation.v
ClassicalExtras.v
Stream.v
Galois.v

TraceModel.v
Properties.v
LanguageModel.v
ChainModel.v
Def.v
TraceCriterion.v
UcoPreservation.v
SafetyDef.v
SafetyCriterion.v
HyperDef.v
HyperCriterion.v
SSCHPreservation.v
SSCHCriterion.v
HSafetyPreservation.v
HSafetyCriterion.v
Relation4Correctness.v
NoTrgGuarantees.v
ANI.v

RobustTraceProperty.v
RobustTraceCriterion.v
UcoRobustPreservation.v
RobustSafetyPreservation.v
RobustSafetyCriterion.v
RobustHyperProperty.v
RobustHyperCriterion.v
RobustSSCHPreservation.v
RobustSSCHCriterion.v
RobustHyperSafetyPreservation.v
RobustHyperSafetyCriterion.v
Robust2relSafetyCriterion.v
Robust2relHyperCriterion.v

Robust2relTraceProperty.v
Robust2relTraceCriterion.v
Robust2relSSCHPreservation.v
Robust2relSSCHCriterion.v
Robust2relSafetyProperty.v
Robust2relHyperProperty.v

ResourceExhaustion.v

UndefBehavior.v
UndefBehaviorCompCert.v

TypeRelationExample.v
ResourceExhaustionExample.v
MoreTargetEventsExample.v

ResourceExhaustion/Maps.v
ResourceExhaustion/Imp.v
ResourceExhaustion/Sequences.v
ResourceExhaustion/Semantics.v
ResourceExhaustion/Compiler.v
ResourceExhaustion/Machine.v
ResourceExhaustion/MachineStackLimited.v
ResourceExhaustion/CompilerStackLimited.v