simple_declare.mli « src « tuto1 « plugin_tutorial « doc - coq - The formal proof system

about summary refs log tree commit diff

path: root/doc/plugin_tutorial/tuto1/src/simple_declare.mli

blob: c55b36742f77df679f9d8221fe1c775e9d1c67b7 (plain)

open Names

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