_CoqProject

-Q theories iris_examples
# 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
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix

theories/barrier/proof.v
theories/barrier/specification.v
theories/barrier/barrier.v
theories/barrier/example_client.v
theories/barrier/example_joining_existentials.v

theories/cl_logic/clprop.v
theories/cl_logic/bi.v
theories/cl_logic/tests.v

theories/lecture_notes/coq_intro_example_1.v
theories/lecture_notes/coq_intro_example_2.v
theories/lecture_notes/lists.v
theories/lecture_notes/lists_guarded.v
theories/lecture_notes/lock.v
theories/lecture_notes/bag.v
theories/lecture_notes/lock_unary_spec.v
theories/lecture_notes/modular_incr.v
theories/lecture_notes/recursion_through_the_store.v
theories/lecture_notes/stack.v
theories/lecture_notes/ccounter.v
theories/lecture_notes/sfra.v
theories/lecture_notes/parallel_incr.v

theories/spanning_tree/graph.v
theories/spanning_tree/mon.v
theories/spanning_tree/spanning.v
theories/spanning_tree/proof.v

theories/concurrent_stacks/specs.v
theories/concurrent_stacks/concurrent_stack1.v
theories/concurrent_stacks/concurrent_stack2.v
theories/concurrent_stacks/concurrent_stack3.v
theories/concurrent_stacks/concurrent_stack4.v

theories/logrel/stlc/lang.v
theories/logrel/stlc/rules.v
theories/logrel/stlc/typing.v
theories/logrel/stlc/logrel.v
theories/logrel/stlc/soundness.v
theories/logrel/stlc/fundamental.v

theories/logrel/persistent_pred.v
theories/logrel/F_mu_ref_conc/base.v
theories/logrel/F_mu_ref_conc/lang.v
theories/logrel/F_mu_ref_conc/wp_rules.v
theories/logrel/F_mu_ref_conc/typing.v
theories/logrel/F_mu_ref_conc/unary/logrel.v
theories/logrel/F_mu_ref_conc/unary/fundamental.v
theories/logrel/F_mu_ref_conc/unary/soundness.v
theories/logrel/F_mu_ref_conc/unary/examples/symbol_nat.v
theories/logrel/F_mu_ref_conc/binary/rules.v
theories/logrel/F_mu_ref_conc/binary/logrel.v
theories/logrel/F_mu_ref_conc/binary/fundamental.v
theories/logrel/F_mu_ref_conc/binary/context_refinement.v
theories/logrel/F_mu_ref_conc/binary/soundness.v
theories/logrel/F_mu_ref_conc/binary/examples/lock.v
theories/logrel/F_mu_ref_conc/binary/examples/counter.v
theories/logrel/F_mu_ref_conc/binary/examples/stack/stack_rules.v
theories/logrel/F_mu_ref_conc/binary/examples/stack/CG_stack.v
theories/logrel/F_mu_ref_conc/binary/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/binary/examples/fact.v

theories/hocap/abstract_bag.v
theories/hocap/cg_bag.v
theories/hocap/fg_bag.v
theories/hocap/exclusive_bag.v
theories/hocap/shared_bag.v
theories/hocap/contrib_bag.v
theories/hocap/lib/oneshot.v
theories/hocap/concurrent_runners.v
theories/hocap/parfib.v

theories/logatom/treiber.v
theories/logatom/treiber2.v
theories/logatom/elimination_stack/hocap_spec.v
theories/logatom/elimination_stack/stack.v
theories/logatom/elimination_stack/spec.v
theories/logatom/flat_combiner/flat.v
theories/logatom/flat_combiner/simple_sync.v
theories/logatom/flat_combiner/sync.v
theories/logatom/flat_combiner/peritem.v
theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
theories/logatom/rdcss/spec.v
theories/logatom/herlihy_wing_queue/spec.v
theories/logatom/herlihy_wing_queue/hwq.v
theories/logatom/counter_with_backup/counter_spec.v
theories/logatom/counter_with_backup/counter_proof.v

theories/proph/lib/one_shot_proph.v
theories/proph/lib/typed_proph.v
theories/proph/eager_coin_spec.v
theories/proph/eager_coin.v
theories/proph/lazy_coin.v
theories/proph/lazy_coin_one_shot.v
theories/proph/lazy_coin_one_shot_typed.v
theories/proph/clairvoyant_coin_spec.v
theories/proph/clairvoyant_coin.v
theories/proph/clairvoyant_coin_typed.v

theories/locks/array_based_queuing_lock/abql.v
theories/locks/freeable_lock/freeable_lock.v
theories/locks/freeable_lock/freeable_logatom_lock.v
theories/locks/freeable_lock/freeable_spin_lock.v