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
---
 kernel/safe_typing.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel/safe_typing.mli')

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
-- 
cgit v1.2.3