Make

-Q . mathcomp.analysis

-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

ereal.v
landau.v

topology_theory/topology.v
topology_theory/bool_topology.v
topology_theory/compact.v
topology_theory/connected.v
topology_theory/matrix_topology.v
topology_theory/nat_topology.v
topology_theory/order_topology.v
topology_theory/product_topology.v
topology_theory/pseudometric_structure.v
topology_theory/subspace_topology.v
topology_theory/subtype_topology.v
topology_theory/supremum_topology.v
topology_theory/topology_structure.v
topology_theory/uniform_structure.v
topology_theory/weak_topology.v
topology_theory/initial_topology.v
topology_theory/num_topology.v
topology_theory/quotient_topology.v
topology_theory/one_point_compactification.v
topology_theory/sigT_topology.v
topology_theory/discrete_topology.v
topology_theory/separation_axioms.v
topology_theory/metric_structure.v
topology_theory/function_spaces.v

homotopy_theory/homotopy.v
homotopy_theory/wedge_sigT.v
homotopy_theory/continuous_path.v

ess_sup_inf.v
cantor.v

normedtype_theory/num_normedtype.v
normedtype_theory/matrix_normedtype.v
normedtype_theory/ereal_normedtype.v
normedtype_theory/pseudometric_normed_Zmodule.v
normedtype_theory/tvs.v
normedtype_theory/normed_module.v
normedtype_theory/complete_normed_module.v
normedtype_theory/urysohn.v
normedtype_theory/vitali_lemma.v
normedtype_theory/normedtype.v

hahn_banach_theorem.v

realfun.v
sequences.v
exp.v
trigo.v
esum.v
derive.v
numfun.v

measure_theory/measurable_structure.v
measure_theory/measure_function.v
measure_theory/counting_measure.v
measure_theory/dirac_measure.v
measure_theory/probability_measure.v
measure_theory/measure_negligible.v
measure_theory/measure_extension.v
measure_theory/measurable_function.v
measure_theory/measure.v

measurable_realfun.v
lebesgue_stieltjes_measure.v
lebesgue_measure.v
borel_hierarchy.v

lebesgue_integral_theory/simple_functions.v
lebesgue_integral_theory/lebesgue_integral_definition.v
lebesgue_integral_theory/measurable_fun_approximation.v
lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
lebesgue_integral_theory/lebesgue_integral_nonneg.v
lebesgue_integral_theory/lebesgue_integrable.v
lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
lebesgue_integral_theory/lebesgue_integral_under.v
lebesgue_integral_theory/lebesgue_Rintegral.v
lebesgue_integral_theory/lebesgue_integral_fubini.v
lebesgue_integral_theory/lebesgue_integral_differentiation.v
lebesgue_integral_theory/lebesgue_integral.v
lebesgue_integral_theory/giry.v

ftc.v
hoelder.v

probability_theory/random_variable.v
probability_theory/bernoulli_distribution.v
probability_theory/binomial_distribution.v
probability_theory/uniform_distribution.v
probability_theory/normal_distribution.v
probability_theory/exponential_distribution.v
probability_theory/poisson_distribution.v
probability_theory/beta_distribution.v
probability_theory/probability.v

convex.v
charge.v
kernel.v
pi_irrational.v
gauss_integral.v
all_analysis.v
showcase/summability.v