package rocq-runtime

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

Source file simple_declare.ml

1
2
3
4
let declare_definition ~poly name sigma body =
  let cinfo = Declare.CInfo.make ~name ~typ:None () in
  let info = Declare.Info.make ~poly () in
  Declare.declare_definition ~info ~cinfo ~opaque:false ~body sigma
OCaml

Innovation. Community. Security.