package rocq-runtime
Module Tuto1_plugin.Simple_declareSource
Source
val declare_definition :
poly:PolyFlags.t ->
Names.Id.t ->
Evd.evar_map ->
EConstr.t ->
Names.GlobRef.t