Make

-R . Algebra

Abelian_group_cat.v 
Abelian_group_facts.v 
Algebra_facts.v 
Algebra.v 
Cantor_Bernstein.v 
Cartesian.v 
Categories2.v 
Categories.v 
Cfield_cat.v 
Cfield_facts.v 
Complex_field.v 
Diff.v 
Endo_set.v 
Field_cat.v 
Field_facts.v 
Fmap.v 
Fpart2.v 
Fpart.v 
Fraction_field.v 
Free_abelian_group.v 
Free_abelian_monoid.v 
Free_group.v 
Free_module.v 
Free_monoid.v 
Generated_group.v 
Generated_module.v 
Generated_monoid.v 
Group_cat.v 
Group_facts.v 
Group_hom_factor.v 
Group_kernel.v 
Group_of_group_hom.v 
Group_power.v 
Group_quotient.v 
Group_util.v 
Hom_module.v 
Ideal.v 
Integral_domain_cat.v 
Integral_domain_facts.v 
Inter.v 
Module_cat.v 
Module_facts.v 
Module_kernel.v 
Module_util.v 
Monoid_cat.v 
Monoid_facts.v 
Monoid_kernel.v 
Monoid_util.v 
Operation_of_monoid.v 
Parts2.v 
Parts3.v 
Parts.v 
Qfield.v 
Ring_cat.v 
Ring_facts.v 
Ring_util.v 
Set_cat.v 
Sets.v 
Sgroup_cat.v 
Sgroup_facts.v 
Singleton.v 
Subcat.v 
Sub_group.v 
Sub_module.v 
Sub_monoid.v 
Sub_sgroup.v 
Tiroirs.v 
Union.v 
Z_group_facts.v 
Z_group.v 
Zring.v 
ZUP.v