Tuto1_plugin.Simple_declare
val declare_definition : poly:bool -> Names.Id.t -> Evd.evar_map -> EConstr.t -> Names.GlobRef.t