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: fd74e81526eb3b47ea8f35613475a9ededf6404e (plain)

open Names
open EConstr

val packed_declare_definition :
    poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit