blob: 73292e01206853c08975dcc39e31181525bf9253 (
plain)
1
2
3
4
5
6
|
let declare_definition ~poly name sigma body =
let udecl = UState.default_univ_decl in
let scope = Locality.Global Locality.ImportDefaultBehavior in
let kind = Decls.(IsDefinition Definition) in
let info = Declare.CInfo.make ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly () in
Declare.declare_definition ~name ~info ~types:None ~body sigma
|
