From 24d8bd2814c9ef89d918ce81d5a0d30fe0662335 Mon Sep 17 00:00:00 2001 From: coq Date: Thu, 9 Jan 2003 16:22:35 +0000 Subject: Export M + Module M <: SIG git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.mli | 33 ++++++++++++++++++++++++++------- 1 file changed, 26 insertions(+), 7 deletions(-) (limited to 'library/declaremods.mli') diff --git a/library/declaremods.mli b/library/declaremods.mli index 9edd051ca..114ea3cf9 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -15,21 +15,36 @@ open Environ open Libnames open Libobject open Lib -(*i*) + (*i*) -(*s This modules provides official fucntions to declare modules and - module types *) +(*s This modules provides official functions to declare modules and + module types *) (*s Modules *) +(* [declare_module interp_modtype interp_modexpr id fargs typ expr] + declares module [id], with type constructed by [interp_modtype] + from functor arguments [fargs] and [typ] and with module body + constructed by [interp_modtype] from functor arguments [fargs] and + by [interp_modexpr] from [expr]. At least one of [typ], [expr] must + be non-empty. + + The [bool] in [typ] tells if the module must be abstracted [true] + with respect to the module type or merely matched without any + restriction [false]. +*) + val declare_module : (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> identifier -> - (identifier list * 'modtype) list -> 'modtype option -> 'modexpr option -> unit - -val start_module : (env -> 'modtype -> module_type_entry) -> - identifier -> (identifier list * 'modtype) list -> 'modtype option -> unit + (identifier list * 'modtype) list -> ('modtype * bool) option -> + 'modexpr option -> unit + +val start_module : (env -> 'modtype -> module_type_entry) -> + identifier -> + (identifier list * 'modtype) list -> ('modtype * bool) option -> + unit val end_module : identifier -> unit @@ -74,6 +89,10 @@ val export_library : val import_module : module_path -> unit +(* [export_module mp] is similar, but is run when the module + containing it is imported *) + +val export_module : module_path -> unit (*s [fold_all_segments] and [iter_all_segments] iterate over all segments, the modules' segments first and then the current -- cgit v1.2.3