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/global.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'library/global.ml') diff --git a/library/global.ml b/library/global.ml index 3129c1caf..d5fafbb8b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -56,12 +56,12 @@ let add_thing add dir id thing = let add_constant = add_thing add_constant let add_mind = add_thing add_mind -let add_modtype = add_thing (fun _ -> add_modtype) () +let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y -let add_module id me = +let add_module id me inl = let l = label_of_id id in - let mp,resolve,new_env = add_module l me !global_env in + let mp,resolve,new_env = add_module l me inl !global_env in global_env := new_env; mp,resolve @@ -70,8 +70,8 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env -let add_include me is_module = - let resolve,newenv = add_include me is_module !global_env in +let add_include me is_module inl = + let resolve,newenv = add_include me is_module inl !global_env in global_env := newenv; resolve @@ -89,8 +89,8 @@ let end_module fs id mtyo = mp,resolve -let add_module_parameter mbid mte = - let resolve,newenv = add_module_parameter mbid mte !global_env in +let add_module_parameter mbid mte inl = + let resolve,newenv = add_module_parameter mbid mte inl !global_env in global_env := newenv; resolve -- cgit v1.2.3