_CoqProject.template

# Disable some Coq warnings associated with Iris.
# See https://gitlab.mpi-sws.org/iris/iris/-/blob/master/_CoqProject.
-arg -w -arg -notation-overridden
# Similar to notation warnings.
-arg -w -arg -custom-entry-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -ambiguous-paths
# Turn warning on hints into error:
-arg -w -arg +deprecated-hint-without-locality
-arg -w -arg +deprecated-instance-without-locality
-arg -w -arg +unknown-option
-arg -w -arg +future-coercion-class-field

-Q rocq-lens/Lens Lens
-Q _build/default/rocq-lens/Lens Lens
-Q rocq-upoly/upoly bedrock.upoly
-Q _build/default/rocq-upoly/upoly bedrock.upoly
-Q rocq-bluerock-brick/theories/prelude bedrock.prelude
-Q _build/default/rocq-bluerock-brick/theories/prelude bedrock.prelude
-Q rocq-bluerock-brick/theories/lang bedrock.lang
-Q _build/default/rocq-bluerock-brick/theories/lang bedrock.lang
-Q rocq-bluerock-brick/theories/noimport bedrock.noimport
-Q _build/default/rocq-bluerock-brick/theories/noimport bedrock.noimport