_CoqProject

-R classical mathcomp.classical
-R theories 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

classical/all_classical.v
classical/boolp.v
classical/contra.v
classical/classical_sets.v
classical/mathcomp_extra.v
classical/functions.v
classical/cardinality.v
classical/fsbigop.v
classical/set_interval.v
theories/all_analysis.v
theories/constructive_ereal.v
theories/ereal.v
theories/reals.v
theories/landau.v
theories/Rstruct.v
theories/topology.v
theories/function_spaces.v
theories/cantor.v
theories/prodnormedzmodule.v
theories/normedtype.v
theories/realfun.v
theories/sequences.v
theories/exp.v
theories/trigo.v
theories/nsatz_realtype.v
theories/esum.v
theories/real_interval.v
theories/lebesgue_measure.v
theories/lebesgue_stieltjes_measure.v
theories/forms.v
theories/derive.v
theories/measure.v
theories/numfun.v
theories/lebesgue_integral.v
theories/ftc.v
theories/hoelder.v
theories/probability.v
theories/summability.v
theories/signed.v
theories/itv.v
theories/convex.v
theories/charge.v
theories/kernel.v
theories/showcase/uniform_bigO.v
theories/altreals/xfinmap.v
theories/altreals/discrete.v
theories/altreals/realseq.v
theories/altreals/realsum.v
theories/altreals/distr.v