-Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
theories/utils/skip.v
theories/utils/llist.v
theories/utils/compare.v
theories/utils/contribution.v
theories/utils/group.v
theories/utils/cofe_solver_2.v
theories/utils/switch.v
theories/channel/proto_model.v
theories/channel/proto.v
theories/channel/channel.v
theories/channel/proofmode.v
theories/examples/basics.v
theories/examples/sort.v
theories/examples/sort_br_del.v
theories/examples/sort_fg.v
theories/examples/map.v
theories/examples/map_reduce.v
theories/examples/subprotocols.v
theories/logrel/model.v
theories/logrel/telescopes.v
theories/logrel/subtyping.v
theories/logrel/environments.v
theories/logrel/term_types.v
theories/logrel/session_types.v
theories/logrel/operators.v
theories/logrel/term_typing_judgment.v
theories/logrel/subtyping_rules.v
theories/logrel/term_typing_rules.v
theories/logrel/lib/mutex.v
theories/logrel/examples/double.v
theories/logrel/examples/pair.v
theories/logrel/examples/rec_subtyping.v
theories/logrel/examples/choice_subtyping.v
theories/logrel/examples/mapper.v