_CoqProject

-Q theories reloc
# 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/prelude/ctx_subst.v
theories/prelude/properness.v
theories/prelude/asubst.v
theories/prelude/bijections.v

theories/logic/spec_ra.v
theories/logic/spec_rules.v
theories/logic/model.v
theories/logic/adequacy.v
theories/logic/proofmode/spec_tactics.v
theories/logic/rules.v
theories/logic/proofmode/tactics.v
theories/logic/derived.v
theories/logic/compatibility.v

theories/typing/types.v
theories/typing/interp.v
theories/typing/fundamental.v
theories/typing/contextual_refinement.v
theories/typing/tactics.v
theories/typing/soundness.v

theories/reloc.v

theories/tests/tp_tests.v
theories/tests/proofmode_tests.v

theories/lib/lock.v
theories/lib/counter.v
theories/lib/Y.v
theories/lib/assert.v
theories/lib/list.v
theories/lib/polyeq.v

theories/examples/bit.v
theories/examples/or.v
theories/examples/namegen.v
theories/examples/cell.v
theories/examples/symbol.v
theories/examples/ticket_lock.v
theories/examples/stack/CG_stack.v
theories/examples/stack/FG_stack.v
theories/examples/stack/refinement.v
theories/examples/various.v
theories/examples/lateearlychoice.v
theories/examples/coinflip.v

theories/examples/par.v

theories/experimental/cka.v

theories/experimental/helping/offers.v
theories/experimental/helping/helping_stack.v

theories/experimental/hocap/counter.v
theories/experimental/hocap/ticket_lock.v