diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:10 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-17 13:31:10 +0000 |
| commit | 77b71db8470553aed0476827ec2e39aed0cbb6ed (patch) | |
| tree | 78503d2a9bae305bbb5b3184a255346107d39ce3 /library/declaremods.mli | |
| parent | a93b81cff868259561c548147dd5ce3267edd6ee (diff) | |
Variant !F M for functor application that does not honor the Inline declarations
For F(X:T), the application !F M works as F M, except that if module type T
contains some "Inline" annotations, they are not taken in account when substituting
X with M in F. See forthcoming commits for examples of use for this feature.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 1db3d95a8..e58f96744 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -41,13 +41,13 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * 'modast) list -> - 'modast Topconstr.module_signature -> - 'modast list -> module_path + (identifier located list * ('modast * bool)) list -> + ('modast * bool) Topconstr.module_signature -> + ('modast * bool) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * 'modast) list -> - 'modast Topconstr.module_signature -> module_path + bool option -> identifier -> (identifier located list * ('modast * bool)) list -> + ('modast * bool) Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -57,12 +57,12 @@ val end_module : unit -> 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 + identifier -> (identifier located list * ('modast * bool)) list -> + ('modast * bool) list -> ('modast * bool) list -> module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * 'modast) list -> - 'modast list -> module_path + identifier -> (identifier located list * ('modast * bool)) list -> + ('modast * bool) list -> module_path val end_modtype : unit -> module_path @@ -106,7 +106,7 @@ val import_module : bool -> module_path -> unit (* Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - 'struct_expr list -> unit + ('struct_expr * bool) list -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented @@ -122,5 +122,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (* For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * module_struct_entry) list -> unit + (mod_bound_id * (module_struct_entry * bool)) list -> unit |