Builders_8 (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Ssralg.GRing.Builders

val coq_Builders_8_V__canonical__eqtype_Equality : 
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Eqtype.Equality.coq_type

val coq_Builders_8_V__canonical__choice_Choice : 
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  Choice.Choice.coq_type

val coq_HB_unnamed_factory_10 : 
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  ('a1, 'a1, 'a1) Coq_isZmodule.phant_axioms ->
  'a1 Coq_isNmodule.axioms_

val coq_Builders_8_V__canonical__GRing_Nmodule : 
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  ('a1, 'a1, 'a1) Coq_isZmodule.phant_axioms ->
  Nmodule.coq_type

val coq_HB_unnamed_factory_12 : 
  'a1 Choice.Coq_hasChoice.axioms_ ->
  'a1 Eqtype.Coq_hasDecEq.axioms_ ->
  ('a1, 'a1, 'a1) Coq_isZmodule.phant_axioms ->
  'a1 Nmodule_isZmodule.axioms_