-Q theories osiris -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files theories/utils/auth_excl.v theories/utils/list.v theories/utils/compare.v theories/utils/contribution.v theories/channel/channel.v theories/channel/proto_model.v theories/channel/proto_channel.v theories/channel/proofmode.v theories/examples/sort.v theories/examples/sort_client.v theories/examples/sort_elem.v theories/examples/loop_sort.v theories/examples/sort_elem_client.v theories/examples/map.v theories/examples/map_reduce.v