From 77b71db8470553aed0476827ec2e39aed0cbb6ed Mon Sep 17 00:00:00 2001 From: letouzey Date: Sun, 17 Jan 2010 13:31:10 +0000 Subject: 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 --- library/declaremods.mli | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'library/declaremods.mli') 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 -- cgit v1.2.3