From df89fbc8ac8d0d485c1a373cb4edbb1835e2c4ad Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 16 Nov 2009 16:52:32 +0000 Subject: 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 --- library/declaremods.mli | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'library/declaremods.mli') 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 -- cgit v1.2.3