boot.v
all_boot.v
eqtype.v
seq.v
ssrAC.v
ssrbool.v
ssreflect.v
ssrfun.v
ssrnat.v
bigop.v
binomial.v
choice.v
div.v
finfun.v
fingraph.v
finset.v
fintype.v
generic_quotient.v
monoid.v
nmodule.v
path.v
prime.v
tuple.v
ssrnotations.v
ssrmatching.v

-I .
-R . mathcomp.boot

# Warnings set as error to avoid (re)introducing them
-arg -w -arg +duplicate-clear
-arg -w -arg +undeclared-scope
-arg -w -arg +deprecated-hint-without-locality
-arg -w -arg +deprecated-hint-rewrite-without-locality
# Warnings we don't really know how to handle
-arg -w -arg -projection-no-head-constant
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -notation-overridden
-arg -w -arg -ambiguous-paths
# introduced in Rocq 9.2
-arg -w -arg +level-tolerance
-arg -w -arg -notation-for-abbreviation
-arg -w -arg -deprecated-lookup-elim-by-name
-arg -w -arg -implicit-create-rewrite-hint-db
# introduced in Rocq 9.3
-arg -w -arg -rewrite-rw
