_CoqProject

-Q src Perennial
-arg -w -arg -ssr-search-moved
-arg -w -arg +deprecated-instance-without-locality
# don't allow ambiguous coercions
-arg -w -arg +ambiguous-paths
-arg -w -arg +deprecated-hint-rewrite-without-locality
-arg -w -arg -deprecated-field-instance-without-locality
-arg -w -arg +deprecated-tactic-notation
-arg -w -arg -deprecated-since-8.19
-arg -w -arg -deprecated-since-8.20
# std lib moved from Coq to Stdlib; will be available in Coq 8.21
-arg -w -arg -deprecated-from-Coq
-arg -w -arg -deprecated-dirpath-Coq
# seems to have false positives
-arg -w -arg -notation-incompatible-prefix
# we haven't updated our code to fix this one
-arg -w -arg -deprecated-typeclasses-transparency-without-locality
# Iris-disabled warnings
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-unknown-warning,-argument-scope-delimiter
-Q external/stdpp/stdpp stdpp
-Q external/stdpp/stdpp_unstable stdpp.unstable
-Q external/stdpp/stdpp_bitvector stdpp.bitvector
-Q external/iris/iris iris
-Q external/iris/iris_deprecated iris.deprecated
-Q external/iris/iris_unstable iris.unstable
-Q external/iris/iris_heap_lang iris.heap_lang
-Q external/coqutil/src/coqutil coqutil
-Q external/Goose Goose
-Q external/record-update/src RecordUpdate
-Q external/coq-tactical/src Tactical
-Q external/iris-named-props/src iris_named_props
-Q new_trusted_code New.code
-Q new_code_axioms New.code
-Q new_partial_axioms New.code_axioms
-Q new New