-Q . mathcomp.experimental_reals

-arg -w -arg -parsing
-arg -w -arg +undeclared-scope
-arg -w -arg +non-primitive-record
-arg -w -arg -ambiguous-paths
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
# introduced in Rocq 9.3
-arg -w -arg -rewrite-rw

xfinmap.v
discrete.v
realseq.v
realsum.v
distr.v
