_CoqProject

-Q theories DiSeL

-arg -w -arg -notation-overridden
-arg -w -arg -local-declaration
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
-arg -w -arg -duplicate-clear
-arg -w -arg -notation-incompatible-format

theories/Core/State.v
theories/Core/Freshness.v
theories/Core/Protocols.v
theories/Core/EqTypeX.v
theories/Core/DepMaps.v
theories/Core/StatePredicates.v
theories/Core/NewStatePredicates.v
theories/Core/Worlds.v
theories/Core/NetworkSem.v
theories/Core/Rely.v
theories/Core/Actions.v
theories/Core/Injection.v
theories/Core/InductiveInv.v
theories/Core/Process.v
theories/Core/Always.v
theories/Core/HoareTriples.v
theories/Core/InferenceRules.v
theories/Core/While.v
theories/Core/DiSeLExtraction.v
theories/Examples/SeqLib.v
theories/Examples/Greeter/Greeter.v
theories/Examples/Querying/QueryProtocol.v
theories/Examples/Querying/QueryHooked.v
theories/Examples/Calculator/CalculatorProtocol.v
theories/Examples/Calculator/CalculatorInvariant.v
theories/Examples/Calculator/CalculatorClientLib.v
theories/Examples/Calculator/CalculatorServerLib.v
theories/Examples/Calculator/SimpleCalculatorServers.v
theories/Examples/Calculator/DelegatingCalculatorServer.v
theories/Examples/Calculator/SimpleCalculatorApp.v
theories/Examples/TwoPhaseCommit/TwoPhaseProtocol.v
theories/Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v
theories/Examples/TwoPhaseCommit/SimpleTPCApp.v
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
theories/Examples/TwoPhaseCommit/TwoPhaseClient.v
theories/Examples/Querying/QueryPlusTPC.v
theories/Examples/LockResource/LockProtocol.v
theories/Examples/LockResource/ResourceProtocol.v
extraction/calculator/CalculatorExtraction.v
extraction/TPC/TwoPhaseExtraction.v