Require Export ring_.
Require Export module_.
Require Export make_small_cat_.
Module Small_Cat_of_Ring_ : A_Cat__ := (Make_Small_Cat_ Ring_).
Test |
Module My_Ring_ : Coeff_Sig_.
Definition R := R.
End My_Ring_.
Module My_Module_Cat_ := (Module_Cat_ My_Ring_).
Module My_Small_Module_Cat_ : A_Cat__ :=
(Make_Small_Cat_ My_Module_Cat_).