diff options
| author | letouzey | 2010-01-17 13:31:10 +0000 |
|---|---|---|
| committer | letouzey | 2010-01-17 13:31:10 +0000 |
| commit | 77b71db8470553aed0476827ec2e39aed0cbb6ed (patch) | |
| tree | 78503d2a9bae305bbb5b3184a255346107d39ce3 /kernel/safe_typing.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 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 169fd158d8..c378d8ccc7 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -55,12 +55,12 @@ val add_mind : (* Adding a module *) val add_module : - label -> module_entry -> safe_environment + label -> module_entry -> bool -> safe_environment -> module_path * delta_resolver * safe_environment (* Adding a module type *) val add_modtype : - label -> module_struct_entry -> safe_environment + label -> module_struct_entry -> bool -> safe_environment -> module_path * safe_environment (* Adding universe constraints *) @@ -76,11 +76,11 @@ val start_module : label -> safe_environment -> module_path * safe_environment val end_module : - label -> module_struct_entry option + label -> (module_struct_entry * bool) option -> safe_environment -> module_path * delta_resolver * safe_environment val add_module_parameter : - mod_bound_id -> module_struct_entry -> safe_environment -> delta_resolver * safe_environment + mod_bound_id -> module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment val start_modtype : label -> safe_environment -> module_path * safe_environment @@ -89,7 +89,7 @@ val end_modtype : label -> safe_environment -> module_path * safe_environment val add_include : - module_struct_entry -> bool -> safe_environment -> + module_struct_entry -> bool -> bool -> safe_environment -> delta_resolver * safe_environment val pack_module : safe_environment -> module_body |