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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/topconstr.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 |
2 files changed, 4 insertions, 0 deletions
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 *) |