Synterp (p.rocq-runtime.9.0.1.doc.rocq-runtime.vernac.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