package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Declaremods.Synterp`Source

val declare_module : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) module_signature ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t
  * module_params_expr
  * module_expr list
  * module_expr module_signature

Source

val start_module : 
  Lib.export ->
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) module_signature ->
  Names.ModPath.t * module_params_expr * module_expr module_signature

Sourceval end_module : unit -> Names.ModPath.t

Sourceval declare_include : (Constrexpr.module_ast * inline) list -> module_expr list

Source

val declare_modtype : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) list ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t * module_params_expr * module_expr list * module_expr list

Source

val start_modtype : 
  Names.Id.t ->
  module_params ->
  (Constrexpr.module_ast * inline) list ->
  Names.ModPath.t * module_params_expr * module_expr list

Sourceval end_modtype : unit -> Names.ModPath.t

Source

val import_module : 
  Libobject.open_filter ->
  export:Lib.export_flag ->
  Names.ModPath.t ->
  unit

Source

val import_modules : 
  export:Lib.export_flag ->
  (Libobject.open_filter * Names.ModPath.t) list ->
  unit

Sourceval register_library : library_name -> library_objects -> unit

Sourceval close_section : unit -> unit

package rocq-runtime

Module Declaremods.SynterpSource

Module `Declaremods.Synterp`Source