diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-16 16:52:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-16 16:52:32 +0000 |
| commit | df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad (patch) | |
| tree | bb0350ce29d299cd7b386667cba8a3fc327d4aa0 /library/declaremods.mli | |
| parent | 8d7e3dc633eef34e0e806c4290aebf1b5a8d753d (diff) | |
New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))
"Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for
"Module M (...). Include M1. Include M2. Include M3... End M."
Moreover M2,M3,etc can be functors as long as they find what they need in what
comes before them (see new command "Include Self").
The only real constraint is that M1,M2,M3,... should not have common elements
(for the moment (?)).
Same behavior for signature : Module Type M := M1 <+ M2 <+ M3.
Note that this <+ is _not_ a primitive construct of the module language,
for instance it cannot be used in signature (Module M <: M1 <+ M2 is
illegal for the moment).
Some example of use in Decidable2 and NZAxioms
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 4a037b005..3d16a287f 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -40,7 +40,7 @@ val declare_module : (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> - 'modexpr option -> module_path + 'modexpr list -> module_path val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> @@ -53,7 +53,8 @@ val end_module : unit -> module_path (*s Module types *) val declare_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> 'modtype -> module_path + identifier -> (identifier located list * 'modtype) list -> + 'modtype list -> module_path val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> module_path @@ -100,7 +101,7 @@ val import_module : bool -> module_path -> unit (* Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr -> bool -> bool -> unit + 'struct_expr -> 'struct_expr list -> bool -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented |