_CoqProject

-R src CoreErlang

src/Basics.v
src/Syntax.v
src/Induction.v
src/Equalities.v
src/SideEffects.v
src/Scoping.v
src/Auxiliaries.v
src/Maps.v
src/Manipulation.v
src/ScopingLemmas.v
src/Matching.v
src/FrameStack/Frames.v
src/FrameStack/SubstSemantics.v
src/FrameStack/Tests/Tests.v
src/FrameStack/Tests/ExceptionTests.v
src/FrameStack/Termination.v
src/FrameStack/SubstSemanticsLemmas.v
src/FrameStack/LogRel.v
src/FrameStack/Compatibility.v
src/FrameStack/CIU.v
src/FrameStack/Examples.v
src/FrameStack/CTX.v

src/Concurrent/PIDRenaming.v
src/Concurrent/ProcessSemantics.v
src/Concurrent/NodeSemantics.v
src/Concurrent/NodeSemanticsLemmas.v
src/Concurrent/StrongBisim.v
src/Concurrent/WeakBisim.v
src/Concurrent/BarbedBisim.v
src/Concurrent/BisimRenaming.v

src/Concurrent/BisimReductions.v
src/Concurrent/MapPmap.v

src/BigStep/Syntax.v
src/BigStep/Induction.v
src/BigStep/Equalities.v
src/BigStep/Helpers.v
src/BigStep/Environment.v
src/BigStep/SideEffects.v
src/BigStep/Auxiliaries.v
src/BigStep/ModuleAuxiliaries.v
src/BigStep/FunctionalBigStep.v
src/BigStep/BigStep.v
src/BigStep/Coverage.v
src/BigStep/Tactics.v
src/BigStep/DeterminismHelpers.v
src/BigStep/SemanticsProofs.v
src/BigStep/SemanticsEquivalence.v
src/BigStep/FullEquivalence.v
src/BigStep/WeakEquivalence.v
src/BigStep/WeakEquivalenceExamples.v
src/BigStep/EquivalenceProofs.v

src/BigStep/MapEval.v
src/BigStep/Tests/AutomatedTests.v
src/BigStep/Tests/AutomatedSideEffectTests.v
src/BigStep/Tests/AutomatedExceptionTests.v
src/BigStep/Tests/AutomatedSideEffectExceptionTests.v