_CoqProject

-Q theories machine_program_logic

-arg -w -arg -notation-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -convert_concl_no_check
-arg -w -arg -undeclared-scope
-arg -w -arg -ambiguous-paths
-arg -w -arg -ssr-search-moved

theories/program_logic/machine.v
theories/program_logic/weakestpre.v
theories/program_logic/adequacy.v