package coq
Module Ring_plugin.G_ringSource
Source
val pr_ring_mod :
Environ.env ->
Evd.evar_map ->
Constrexpr.constr_expr Ring_ast.ring_mod ->
Pp.tSource
val pr_ring_mods :
Environ.env ->
Evd.evar_map ->
Constrexpr.constr_expr Ring_ast.ring_mod list ->
Pp.tSource
val wit_ring_mods :
(Constrexpr.constr_expr Ring_ast.ring_mod list, unit, unit)
Genarg.genarg_typeSource
val pr_field_mod :
Environ.env ->
Evd.evar_map ->
Constrexpr.constr_expr Ring_ast.field_mod ->
Pp.tSource
val wit_field_mod :
(Constrexpr.constr_expr Ring_ast.field_mod, unit, unit) Genarg.genarg_typeSource
val pr_field_mods :
Environ.env ->
Evd.evar_map ->
Constrexpr.constr_expr Ring_ast.field_mod list ->
Pp.tSource
val wit_field_mods :
(Constrexpr.constr_expr Ring_ast.field_mod list, unit, unit)
Genarg.genarg_type