_CoqProject

-R . project

-arg -nois

-arg -w
-arg all

#-arg -debug

./src/Init/notations.v
./src/Init/coq_logic.v
./src/Init/base_logic.v
./src/Init/logic.v
./src/Init/tactics.v
./src/Init/tlc_tactics.v
./src/Init/types.v
./src/Init/function.v
./src/Init/init.v

./src/Algebra/Plus/plus_group.v

./src/Algebra/Mult/mult_ring.v
./src/Algebra/Mult/mult_field.v

./src/Algebra/Relation/relation.v
./src/Algebra/Relation/order_bounds.v
./src/Algebra/Relation/order_plus.v
./src/Algebra/Relation/order_mult.v
./src/Algebra/Relation/order_minmax.v
./src/Algebra/Relation/order_abs.v
./src/Algebra/Relation/order_self_abs.v
./src/Algebra/Relation/order_dict.v
./src/Algebra/Relation/order_cone.v

./src/Number/Nat/nat_base.v
./src/Number/Nat/nat_plus.v
./src/Number/Nat/nat_mult.v
./src/Number/Nat/nat_order.v
./src/Number/Nat/nat_minus.v
./src/Number/Nat/nat_binom.v
./src/Number/Nat/nat_sum.v
./src/Number/Nat/nat_abstract.v
./src/Number/Nat/nat_from.v
./src/Number/Nat/nat.v

./src/Set/set_base.v
./src/Set/set_set.v
./src/Set/set_type.v
./src/Set/set_function.v
./src/Set/set_order.v
./src/Set/set_induction.v
./src/Set/equivalence.v
./src/Set/set_finite.v
./src/Set/zorn.v
./src/Set/zorn_set.v
./src/Set/zorn_preorder.v
./src/Set/zorn_unary_function.v
./src/Set/zorn_binary_function.v
./src/Set/well_order.v
./src/Set/set.v

./src/List/list_base.v
./src/List/list_in.v
./src/List/list_set.v
./src/List/list_nat.v
./src/List/list_fold.v
./src/List/list_perm.v
./src/List/list.v
./src/List/unordered_list_base.v
./src/List/unordered_list_in.v
./src/List/unordered_list_set.v
./src/List/unordered_list_nat.v
./src/List/unordered_list_fold.v
./src/List/unordered_list.v

./src/Category/category_def.v
./src/Category/category_base.v
./src/Category/category_functor.v
./src/Category/category_natural_transformation.v
./src/Category/category_equivalence.v
./src/Category/category_initterm.v
./src/Category/category_product.v
./src/Category/category_coproduct.v
./src/Category/category_comma.v

./src/Category/basic_categories.v
./src/Algebra/Plus/monoid_category.v
./src/Algebra/Plus/group_category.v
./src/Algebra/Mult/ring_category.v
./src/Algebra/Mult/domain_category.v
./src/Algebra/Mult/field_category.v
./src/Algebra/Relation/ordered_domain_category.v
./src/Algebra/Relation/ordered_field_category.v

./src/Number/Int/int_base.v
./src/Number/Int/int_plus.v
./src/Number/Int/int_mult.v
./src/Number/Int/int_order.v
./src/Number/Int/int_abstract.v
./src/Number/Int/int_from.v
./src/Number/Int/int.v

./src/Algebra/Ring/Fraction/fraction_base.v
./src/Algebra/Ring/Fraction/fraction_plus.v
./src/Algebra/Ring/Fraction/fraction_mult.v
./src/Algebra/Ring/Fraction/fraction_order.v
./src/Algebra/Ring/Fraction/fraction_category.v
./src/Number/Rat/rat.v

./src/Set/Ordinal/ord_base.v
./src/Set/Ordinal/ord_order.v
./src/Set/Ordinal/ord_plus.v
./src/Set/Ordinal/ord_mult.v
./src/Set/Ordinal/ord_basic.v
./src/Set/Ordinal/ord_induction.v
./src/Set/Ordinal/ord_pow_def.v
./src/Set/Ordinal/ord_pow.v

./src/Set/Cardinal/card_base.v
./src/Set/Cardinal/card_order.v
./src/Set/Cardinal/card_plus.v
./src/Set/Cardinal/card_mult.v
./src/Set/Cardinal/card_pow.v
./src/Set/Cardinal/card_nat.v
./src/Set/Cardinal/card_infinite1.v
./src/Set/Cardinal/card_infinite2.v
./src/Set/Cardinal/card_infinite3.v
./src/Set/Cardinal/card_types.v
./src/Set/Cardinal/card_real_interval.v
./src/Set/Cardinal/card_real.v
./src/Set/Cardinal/card.v

./src/Number/Real/Cauchy/cauchy_real_base.v
./src/Number/Real/Cauchy/cauchy_real_plus.v
./src/Number/Real/Cauchy/cauchy_real_mult.v
./src/Number/Real/Cauchy/cauchy_real_order.v
./src/Number/Real/Cauchy/cauchy_real_complete.v
./src/Number/Real/Cauchy/cauchy_real.v
./src/Number/Real/real_base.v
./src/Number/Real/real.v

./src/Number/Complex/complex_base.v
./src/Number/Complex/complex_plus.v
./src/Number/Complex/complex_mult.v
./src/Number/Complex/complex.v

./src/Algebra/Group/group_subgroup.v
./src/Algebra/Group/group_order.v

./src/Algebra/Ring/ring_ideal.v
./src/Algebra/Ring/Domain/mult_div.v
./src/Algebra/Ring/Domain/euclidean_domain.v
./src/Algebra/Ring/Domain/gcd.v
./src/Algebra/Ring/Domain/principle_ideal.v
./src/Algebra/Ring/Domain/factorization.v
./src/Algebra/Ring/Domain/nat_domain.v

./src/Algebra/Linear/Base/linear_base.v
./src/Algebra/Linear/Base/module_category.v
./src/Algebra/Linear/Base/algebra_category.v
./src/Algebra/Linear/Base/linear_combination.v
./src/Algebra/Linear/Base/linear_bilinear.v
./src/Algebra/Linear/Base/linear_bilinear_form.v
./src/Algebra/Linear/Base/linear_subspace.v
./src/Algebra/Linear/Base/linear_span.v
./src/Algebra/Linear/Examples/linear_transformation_space.v
./src/Algebra/Linear/Examples/linear_sum.v
./src/Algebra/Linear/Examples/linear_unital_zero.v
./src/Algebra/Linear/Grade/linear_sum_module.v
./src/Algebra/Linear/Grade/linear_grade.v
./src/Algebra/Linear/Grade/linear_grade_sum.v
./src/Algebra/Linear/Grade/linear_free.v
./src/Algebra/Linear/Grade/linear_grade_isomorphism.v
./src/Algebra/Linear/Grade/linear_extend.v
./src/Algebra/Linear/Grade/linear_basis.v

./src/Algebra/Ring/Polynomial/polynomial_base.v
./src/Algebra/Ring/Polynomial/polynomial_degree.v

./src/Algebra/Linear/Tensor/Product/tensor_product_construction.v
./src/Algebra/Linear/Tensor/Product/tensor_product_universal.v
./src/Algebra/Linear/Tensor/Product/tensor_product_isomorphisms.v
./src/Algebra/Linear/Tensor/Product/tensor_product_assoc.v
./src/Algebra/Linear/Tensor/Product/tensor_product.v
./src/Algebra/Linear/Tensor/Power/tensor_power_base.v
./src/Algebra/Linear/Tensor/Power/tensor_power_universal.v
./src/Algebra/Linear/Tensor/Power/tensor_power.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra_defs.v
./src/Algebra/Linear/Tensor/Algebra/Traditional/tensor_algebra_traditional_base.v
./src/Algebra/Linear/Tensor/Algebra/Traditional/tensor_algebra_traditional_mult.v
./src/Algebra/Linear/Tensor/Algebra/Traditional/tensor_algebra_traditional_scalar.v
./src/Algebra/Linear/Tensor/Algebra/Traditional/tensor_algebra_traditional_vector.v
./src/Algebra/Linear/Tensor/Algebra/Traditional/tensor_algebra_traditional_universal.v
./src/Algebra/Linear/Tensor/Algebra/Direct/tensor_algebra_direct_base.v
./src/Algebra/Linear/Tensor/Algebra/Direct/tensor_algebra_direct_universal.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra_base.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra_inclusions.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra_grade1.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra_grade2.v
./src/Algebra/Linear/Tensor/Algebra/tensor_algebra.v

./src/Algebra/Geometric/Construction/geometric_construct.v
./src/Algebra/Geometric/Construction/geometric_universal.v
./src/Algebra/Geometric/Construction/geometric_sum.v
./src/Algebra/Geometric/Construction/geometric_involutions.v
./src/Algebra/Geometric/Construction/exterior_base.v
./src/Algebra/Geometric/Construction/exterior_grade1.v
./src/Algebra/Geometric/Construction/exterior_grade2.v
./src/Algebra/Geometric/Construction/exterior_involutions.v
./src/Algebra/Geometric/Construction/geometric_to_exterior.v
./src/Algebra/Geometric/Construction/exterior_to_geometric.v
./src/Algebra/Geometric/Construction/geometric_exterior_isomorphism.v
./src/Algebra/Geometric/Construction/geometric_grade.v
./src/Algebra/Geometric/Construction/geometric_involutions_grade.v
./src/Algebra/Geometric/Construction/geometric_decomposition.v
./src/Algebra/Geometric/Construction/geometric_base.v

./src/Algebra/Geometric/geometric_norm.v
./src/Algebra/Geometric/geometric_inner.v
./src/Algebra/Geometric/geometric_outer.v
./src/Algebra/Geometric/geometric_product_formulae.v
./src/Algebra/Geometric/geometric_versor.v

./src/Topology/topology_base.v
./src/Topology/topology_basis.v
./src/Topology/topology_subbasis.v
./src/Topology/topology_order_base.v
./src/Topology/topology_order.v
./src/Topology/topology_order2.v
./src/Topology/topology_product.v
./src/Topology/topology_subspace.v
./src/Topology/topology_closure.v
./src/Topology/topology_limit.v
./src/Topology/topology_axioms.v
./src/Topology/topology_continuous.v
./src/Topology/topology_homeo.v
./src/Topology/topology_connected.v
./src/Topology/topology_real.v
./src/Topology/topology_path.v
./src/Topology/topology_compact.v
./src/Topology/topology_function_limit.v
./src/Topology/topology_finite_complement.v
./src/Topology/all_topology_base.v
./src/Topology/all_topology_single.v
./src/Topology/all_topology_topologies.v

./src/Analysis/analysis_base.v
./src/Analysis/analysis_topology.v
./src/Analysis/analysis_sequence.v
./src/Analysis/analysis_continuous.v
./src/Analysis/analysis_subspace.v
./src/Analysis/analysis_compact.v
./src/Analysis/analysis_function.v
./src/Analysis/analysis_basic.v

./src/Analysis/Norm/analysis_norm.v
./src/Analysis/Norm/analysis_series.v
./src/Analysis/Norm/norm_continuous.v
./src/Analysis/Norm/norm_mult.v
./src/Analysis/Norm/analysis_geometric.v
./src/Analysis/Norm/analysis_linear.v
./src/Analysis/Norm/analysis_bilinear.v
./src/Analysis/Norm/norm_function.v
./src/Analysis/Norm/analysis_scalar.v
./src/Analysis/Norm/analysis_algebraic.v

./src/Analysis/Real/analysis_order.v
./src/Analysis/Real/analysis_func_order.v
./src/Analysis/Real/real_ivt.v
./src/Analysis/Real/real_sqrt.v
./src/Analysis/Real/analysis_real.v

./src/Analysis/Differential/analysis_frechet_derivative.v
./src/Analysis/Differential/analysis_frechet_bilinear.v
./src/Analysis/Differential/derivative.v
./src/Analysis/Differential/real_derivative.v

./src/Number/Real/Dedekind/dedekind_real_base.v
./src/Number/Real/Dedekind/dedekind_real_order.v
./src/Number/Real/Dedekind/dedekind_real_plus.v
./src/Number/Real/Dedekind/dedekind_real_mult1.v
./src/Number/Real/Dedekind/dedekind_real_mult2.v
./src/Number/Real/Dedekind/dedekind_real_mult3.v
./src/Number/Real/Dedekind/dedekind_real.v

./src/Number/Real/Zorn/zorn_real_base.v
./src/Number/Real/Zorn/zorn_real_arch.v
./src/Number/Real/Zorn/zorn_real_zorn.v
./src/Number/Real/Zorn/zorn_real_analysis.v
./src/Number/Real/Zorn/zorn_real_quotient.v
./src/Number/Real/Zorn/zorn_real_complete.v
./src/Number/Real/Zorn/zorn_real.v