_CoqProject

-Q src/guarding guarding

src/guarding/internal/auth_frag_util.v
src/guarding/internal/wsat_util.v
src/guarding/internal/factoring_upred.v
src/guarding/internal/inved.v

src/guarding/own_and.v
src/guarding/own_and_own_sep.v
src/guarding/factoring_props.v
src/guarding/guard.v
src/guarding/tactics.v
src/guarding/guard_later_pers.v

src/guarding/storage_protocol/protocol.v
src/guarding/storage_protocol/base_storage_opt.v

src/guarding/lib/lifetime.v
src/guarding/lib/cancellable.v
src/guarding/lib/non_atomic_map.v
src/guarding/lib/rwlock.v

-Q src/lang lang

src/lang/adequacy.v
src/lang/class_instances.v
src/lang/heap_ra.v
src/lang/lang.v
src/lang/notation.v
src/lang/primitive_laws.v
src/lang/proofmode.v
src/lang/simp.v
src/lang/tactics.v

-Q src/examples examples

src/examples/rwlock.v
src/examples/forever.v
src/examples/gmap_option.v
src/examples/hash_table_raw.v
src/examples/misc_tactics.v
src/examples/hash_table_logic.v
src/examples/hash_table.v
src/examples/seqs.v
src/examples/main.v
src/examples/fractional.v
src/examples/counting.v
src/examples/heap_lang_wp_load_shared.v

-arg -w -arg -argument-scope-delimiter
-arg -w -arg -notation-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -unknown-warning
-arg -w -arg -argument-scope-delimiter
-arg -w -arg -notation-incompatible-prefix