Source file simple_declare.ml

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 cinfo = Declare.CInfo.make ~name ~typ:None () in
  let info = Declare.Info.make ~scope ~kind  ~udecl ~poly () in
  Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma