diff options
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index e3eb38af6..093d43934 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -113,6 +113,9 @@ let subst_scope (subst,sc) = sc open Libobject +let discharge_scope (local,_,_ as o) = + if local then None else Some o + let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o @@ -479,16 +482,18 @@ let classify_arguments_scope (req,_,_ as obj) = if req = ArgsScopeNoDischarge then Dispose else Substitute obj let rebuild_arguments_scope (req,r,l) = + let req' = + if isVarRef r && Lib.is_in_section r then ArgsScopeNoDischarge else req in match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - (req,r,compute_arguments_scope (Global.type_of_global r)) + (req',r,compute_arguments_scope (Global.type_of_global r)) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section *) let l' = compute_arguments_scope (Global.type_of_global r) in let l1,_ = list_chop (List.length l' - List.length l) l' in - (req,r,l1@l) + (req',r,l1@l) let (inArgumentsScope,outArgumentsScope) = declare_object {(default_object "ARGUMENTS-SCOPE") with @@ -499,11 +504,14 @@ let (inArgumentsScope,outArgumentsScope) = discharge_function = discharge_arguments_scope; rebuild_function = rebuild_arguments_scope } +let is_local local ref = local || (isVarRef ref && not (Lib.is_in_section ref)) + let declare_arguments_scope_gen req r scl = Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) let declare_arguments_scope local ref scl = - let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in + let req = + if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in declare_arguments_scope_gen req ref scl let find_arguments_scope r = |