_CoqProject

-Q theories iris_ni
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths

theories/heap_lang/lang_det.v
theories/program_logic/dwp.v
theories/program_logic/lifting.v
theories/program_logic/ectx_lifting.v
theories/program_logic/classes.v
theories/program_logic/heap_lang_lifting.v
theories/program_logic/dwp_adequacy.v
theories/proofmode/dwp_tactics.v
theories/logrel/slevel.v
theories/logrel/types.v
theories/logrel/interp.v
theories/logrel/typing.v
theories/examples/value_dep.v
theories/examples/rand.v
theories/examples/lock.v
theories/examples/ticket_lock.v
theories/examples/par.v
theories/examples/value_sensitivity.v
theories/examples/value_sensitivity_2.v
theories/examples/value_sensitivity_3.v
theories/examples/value_sensitivity_4.v
theories/examples/various.v
theories/examples/multiset.v
# theories/examples/allocator.v
theories/examples/array.v
theories/examples/set.v
theories/examples/calendar.v