Synterp (coq-core.Declaremods.Synterp)

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

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

val end_module : unit -> Names.ModPath.t

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

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

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

val end_modtype : unit -> Names.ModPath.t

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

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

val register_library : library_name -> library_objects -> unit