_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 bluerock.upoly
-Q _build/default/rocq-upoly/upoly bluerock.upoly
-Q rocq-bluerock-brick/theories/prelude bluerock.prelude
-Q _build/default/rocq-bluerock-brick/theories/prelude bluerock.prelude
-Q rocq-bluerock-brick/theories/lang bluerock.lang
-Q _build/default/rocq-bluerock-brick/theories/lang bluerock.lang
-Q rocq-bluerock-brick/theories/noimport bluerock.noimport
-Q _build/default/rocq-bluerock-brick/theories/noimport bluerock.noimport