_CoqProject

-Q Structures Bythos.Structures
-Q Systems Bythos.Systems
-Q Properties Bythos.Properties
-Q Utils Bythos.Utils
-Q Protocols Bythos.Protocols
-Q Composition Bythos.Composition

# Referring to the submodules
-Q coqtla/src TLA
-Q coqtla/external/stdpp/stdpp stdpp
-Q coqtla/external/stdpp/stdpp_unstable stdpp.unstable
-Q coqtla/external/coq-record-update RecordUpdate

-arg -w -arg -notation-overridden
-arg -w -arg -local-declaration
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant

Structures/Types.v
Structures/Address.v
Systems/Protocol.v
Systems/States.v
Systems/Network.v
Properties/Invariant.v
Properties/Liveness.v
Properties/Liveness_tla.v
Utils/Misc.v
Utils/ListFacts.v
Utils/TLAmore.v
Utils/Tactics.v
Utils/Fintype.v
# Utils/InfSeqAdaptor.v

Protocols/ABC/Types.v
Protocols/ABC/Protocol.v
Protocols/ABC/Network.v
Protocols/ABC/Invariant.v
Protocols/ABC/Safety.v
Protocols/ABC/Liveness.v
Protocols/ABC/Liveness_tla.v

Protocols/RB/Types.v
Protocols/RB/Protocol.v
Protocols/RB/Network.v
Protocols/RB/Invariant.v
Protocols/RB/Safety.v
Protocols/RB/Liveness.v
Protocols/RB/Liveness_tla.v

# Protocols/ABC/OldProofs/Protocol.v
# Protocols/ABC/OldProofs/Network.v
# Protocols/ABC/OldProofs/Invariant.v
# Protocols/ABC/OldProofs/Liveness_tla.v

Protocols/PB/Types.v
Protocols/PB/Protocol.v
Protocols/PB/Network.v
Protocols/PB/Invariant.v
Protocols/PB/Safety.v
Protocols/PB/Liveness.v
Protocols/PB/Liveness_tla.v

Protocols/PB/Iterated/PB2.v
Protocols/PB/Iterated/PB3.v

Protocols/RBABC/Types.v
Protocols/RBABC/Protocol.v
Protocols/RBABC/Liveness_tla.v

Composition/Types.v
Composition/Protocol.v
Composition/States.v
Composition/Network.v
Composition/Liveness_tla.v

Extraction/Driver.v