package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file simple_declare.ml

1
2
3
4
5
6
7
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
OCaml

Innovation. Community. Security.