_CoqProject

-Q theories logrel_ifc
-Q vendor/modal-weakestpre/theories mwp

-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

theories/prelude/base.v

theories/lambda_sec/lang.v
theories/lambda_sec/lattice.v
theories/lambda_sec/types.v
theories/lambda_sec/typing.v
theories/lambda_sec/rules_unary.v
theories/lambda_sec/logrel_label.v
theories/lambda_sec/logrel_unary.v
theories/lambda_sec/fundamental_unary.v
theories/lambda_sec/rules_binary.v
theories/lambda_sec/logrel_binary.v
theories/lambda_sec/fundamental_binary.v
theories/lambda_sec/noninterference.v
theories/lambda_sec/notation.v

# examples
theories/examples/arith.v
theories/examples/awkward.v
theories/examples/high_observer.v
theories/examples/lambda_service.v
theories/examples/leak_fun.v
theories/examples/lists.v
theories/examples/parametricity.v
theories/examples/refs_implicit.v
theories/examples/refs.v
theories/examples/report.v
theories/examples/value_dependent.v
theories/examples/value_dependent_pack.v
theories/examples/value_dependent_pack_no_ref.v
theories/examples/value_dependent_pack_no_ref_no_bool.v
theories/examples/existential_decl.v
# theories/examples/compute_with_cache.v