diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
| commit | 9b6517c0c933fb1d66c7feb53fa57e1697d8124a (patch) | |
| tree | d914d6bc2c5598baad03807ce40ada0b1d56045d /library/declaremods.mli | |
| parent | e3e6ff629e258269bc9fe06f7be99a2d5f334071 (diff) | |
Include can accept both Module and Module Type
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index ae0b0aa10..1db3d95a8 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,16 +37,17 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_struct_entry) -> - (env -> 'modexpr -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * 'modtype) list -> - 'modtype Topconstr.module_signature -> - 'modexpr list -> module_path + (identifier located list * 'modast) list -> + 'modast Topconstr.module_signature -> + 'modast list -> module_path -val start_module : (env -> 'modtype -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * 'modtype) list -> - 'modtype Topconstr.module_signature -> module_path +val start_module : (env -> 'modast -> module_struct_entry) -> + bool option -> identifier -> (identifier located list * 'modast) list -> + 'modast Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -54,13 +55,14 @@ val end_module : unit -> module_path (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> - 'modtype list -> 'modtype list -> module_path +val declare_modtype : (env -> 'modast -> module_struct_entry) -> + (env -> 'modast -> module_struct_entry * bool) -> + identifier -> (identifier located list * 'modast) list -> + 'modast list -> 'modast list -> module_path -val start_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> - 'modtype list -> module_path +val start_modtype : (env -> 'modast -> module_struct_entry) -> + identifier -> (identifier located list * 'modast) list -> + 'modast list -> module_path val end_modtype : unit -> module_path @@ -103,8 +105,8 @@ val import_module : bool -> module_path -> unit (* Include *) -val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr list -> bool -> unit +val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> + 'struct_expr list -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented |