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
---
 interp/topconstr.ml  | 2 ++
 interp/topconstr.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d93e1ab140..a20cd1bc23 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1009,6 +1009,8 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
+
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1b1698f956..3b5832f18c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -246,6 +246,8 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
+
 type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
-- 
cgit v1.2.3