blob: 5431a21b53a0565f14cca5a27adb2b8ff92fca07 (
plain)
1
2
3
4
5
6
|
let declare_definition ~poly name sigma body =
let udecl = UState.default_univ_decl in
let scope = Declare.Global Declare.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
|
