-Q theories iris_examples -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files theories/barrier/proof.v theories/barrier/specification.v theories/barrier/barrier.v theories/barrier/protocol.v
theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v
