package coq
Module Tuto1_plugin.Simple_declareSource
Source
val declare_definition :
poly:bool ->
Names.Id.t ->
Evd.evar_map ->
EConstr.t ->
Names.GlobRef.t