-Q theories actris # We sometimes want to locally override notation, and there is no good way to do that with scopes. -arg -w -arg -notation-overridden # Cannot use non-canonical projections as it causes massive unification failures # (https://github.com/coq/coq/issues/6294). -arg -w -arg -redundant-canonical-projection 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/swap_mapper.v theories/examples/subprotocols.v theories/examples/list_rev.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/session_typing_rules.v theories/logrel/napp.v theories/logrel/lib/mutex.v theories/logrel/lib/par_start.v theories/logrel/examples/pair.v theories/logrel/examples/par_recv.v theories/logrel/examples/rec_subtyping.v theories/logrel/examples/choice_subtyping.v theories/logrel/examples/mapper.v theories/logrel/examples/mapper_list.v theories/logrel/examples/compute_service.v theories/logrel/examples/compute_client_list.v