_CoqProject

-R Requisite Requisite
-R Logic Logic
-R Numbers Numbers
-R Subsets Subsets
-R Algebra Algebra
-R Lebesgue Lebesgue
-R LM LM
-R FEM FEM

# To hide warnings about notations redefined in SSReflect/MathComp
-arg "-w -notation-overridden"
-arg "-w -hiding-delimiting-key"
# To hide warnings about coercion in Coquelicot
-arg "-w -ambiguous-paths"

-docroot .

#
# Requisite.
#

./Requisite/stdlib.v
./Requisite/stdlib_wR.v
./Requisite/ssr.v
./Requisite/ssr_wMC.v

#
# Logic.
#

./Logic/logic_compl.v

# For LM.
./Logic/logic_tricks.v

#
# Numbers.
#

./Numbers/nat_compl.v
./Numbers/countable_sets.v

# Coming from LM.
./Numbers/R_compl.v

./Numbers/Numbers_wDep.v

#
# Subsets.
#

./Subsets/FinBij.v
./Subsets/Subset.v
./Subsets/Subset_dec.v
./Subsets/Subset_charac.v
./Subsets/Subset_finite.v
./Subsets/Subset_any.v
./Subsets/Subset_seq.v

./Subsets/Function.v
./Subsets/Function_sub.v
./Subsets/Sub_type.v
./Subsets/Binary_relation.v

./Subsets/ord_compl.v
./Subsets/Finite_family.v
./Subsets/Finite_table.v

./Subsets/Subsets.v
./Subsets/Subsets_wDep.v

#
# Algebra.
#

./Algebra/Hierarchy_compl.v
./Algebra/Sub_struct.v

./Algebra/Monoid/Monoid_compl.v
./Algebra/Monoid/Monoid_FF.v
./Algebra/Monoid/Monoid_FT.v
./Algebra/Monoid/Monoid_sum.v
./Algebra/Monoid/Monoid_morphism.v
./Algebra/Monoid/Monoid_sub.v
./Algebra/Monoid/MonoidMult.v
./Algebra/Monoid/MonoidComp.v
./Algebra/Monoid/ConcatnF.v
./Algebra/Monoid/Monomial_order.v
./Algebra/Monoid/Monoid.v

./Algebra/Group/Group_compl.v
./Algebra/Group/Group_morphism.v
./Algebra/Group/Group_sub.v
./Algebra/Group/GroupMult.v
./Algebra/Group/Group.v

./Algebra/Ring/Ring_compl.v
./Algebra/Ring/Ring_FF_FT.v
./Algebra/Ring/Ring_charac.v
./Algebra/Ring/Ring_kron.v
./Algebra/Ring/Ring_morphism.v
./Algebra/Ring/Ring_sub.v
./Algebra/Ring/Ring.v

./Algebra/ModuleSpace/ModuleSpace_compl.v
./Algebra/ModuleSpace/ModuleSpace_FF_FT.v
./Algebra/ModuleSpace/ModuleSpace_lin_comb.v
./Algebra/ModuleSpace/ModuleSpace_lin_map.v
./Algebra/ModuleSpace/ModuleSpace_sub.v
./Algebra/ModuleSpace/ModuleSpace_R_compl.v
./Algebra/ModuleSpace/ModuleSpace.v

./Algebra/AffineSpace/AffineSpace_def.v
./Algebra/AffineSpace/AffineSpace_FF.v
./Algebra/AffineSpace/AffineSpace_baryc.v
./Algebra/AffineSpace/AffineSpace_aff_map.v
./Algebra/AffineSpace/AffineSpace_sub.v
./Algebra/AffineSpace/AffineSpace.v

./Algebra/Finite_dim/matrix.v
./Algebra/Finite_dim/Finite_dim_MS_def.v
./Algebra/Finite_dim/Finite_dim_MS_lin_span.v
./Algebra/Finite_dim/Finite_dim_MS_lin_gen.v
./Algebra/Finite_dim/Finite_dim_MS_lin_indep.v
./Algebra/Finite_dim/Finite_dim_MS_basis.v
./Algebra/Finite_dim/Finite_dim_MS_lin_map.v
./Algebra/Finite_dim/Finite_dim_MS_lin_indep_R.v
./Algebra/Finite_dim/Finite_dim_MS_basis_R.v
./Algebra/Finite_dim/Finite_dim_MS_lin_map_R.v
./Algebra/Finite_dim/Finite_dim_MS_duality_R.v
./Algebra/Finite_dim/Finite_dim_MS.v
./Algebra/Finite_dim/Finite_dim_AS_def.v
./Algebra/Finite_dim/Finite_dim_AS_aff_span.v
./Algebra/Finite_dim/Finite_dim_AS_aff_gen.v
./Algebra/Finite_dim/Finite_dim_AS_aff_indep.v
./Algebra/Finite_dim/Finite_dim_AS_aff_basis.v
./Algebra/Finite_dim/Finite_dim_AS.v
./Algebra/Finite_dim/Finite_dim.v

./Algebra/binomial_compl.v

./Algebra/Algebra.v
./Algebra/Algebra_wDep.v

#
# Lebesgue integration.
#

./Lebesgue/subset_compl.v
./Lebesgue/list_compl.v
./Lebesgue/sort_compl.v
./Lebesgue/R_compl.v
./Lebesgue/LF_subcover.v
./Lebesgue/Rbar_compl.v
./Lebesgue/UniformSpace_compl.v
./Lebesgue/topo_bases_R.v
./Lebesgue/sum_Rbar_nonneg.v

./Lebesgue/sigma_algebra.v
./Lebesgue/sigma_algebra_R_Rbar.v

./Lebesgue/Subset_system_def.v
./Lebesgue/Subset_system_base.v
./Lebesgue/Subset_system_gen.v
./Lebesgue/Subset_system.v

./Lebesgue/measurable_fun.v

./Lebesgue/measure.v
./Lebesgue/measure_uniq.v
./Lebesgue/measure_R.v

./Lebesgue/simple_fun.v
./Lebesgue/Mp.v
./Lebesgue/LInt_p.v
./Lebesgue/Tonelli.v

./Lebesgue/Lebesgue_p.v
./Lebesgue/Lebesgue_p_wDep.v

./Lebesgue/Bochner/square_bij.v
./Lebesgue/Bochner/series.v
./Lebesgue/Bochner/complete_normed_module_series.v
./Lebesgue/Bochner/hierarchy_notations.v
./Lebesgue/Bochner/Rmax_n.v
./Lebesgue/Bochner/topology_compl.v
./Lebesgue/Bochner/simpl_fun.v
./Lebesgue/Bochner/CUS_Lim_seq.v
./Lebesgue/Bochner/BInt_sf.v
./Lebesgue/Bochner/Bsf_Lsf.v
./Lebesgue/Bochner/Bi_fun.v
./Lebesgue/Bochner/BInt_Bif.v
./Lebesgue/Bochner/BInt_LInt_p.v
./Lebesgue/Bochner/BInt_R.v
./Lebesgue/Bochner/B_spaces.v
./Lebesgue/Bochner/Bochner.v
./Lebesgue/Bochner/Bochner_wDep.v

#
# Lax-Milgram theorem.
#

./LM/fixed_point.v
./LM/direct_sum.v
./LM/hilbert.v
./LM/continuous_linear_map.v
./LM/hierarchyD.v
./LM/lax_milgram.v
./LM/lax_milgram_cea.v
./LM/finitedim.v

#
# Finite-element method.
#

./FEM/geometry.v
./FEM/monomial.v
./FEM/multi_index.v
./FEM/poly_Pdk.v
./FEM/geom_simplex.v
./FEM/poly_LagPd1_ref.v
./FEM/geom_transf_affine.v
./FEM/poly_LagPd1_cur.v
./FEM/poly_LagP1k.v
./FEM/FE.v
./FEM/FE_transf.v
./FEM/FE_LagP.v