diff options
| -rw-r--r-- | interp/notation.ml | 29 | ||||
| -rw-r--r-- | library/impargs.ml | 4 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 2 |
4 files changed, 21 insertions, 16 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index d0734b3d8..3989f0072 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -446,9 +446,10 @@ let rec compute_arguments_scope t = let arguments_scope = ref Refmap.empty -type arguments_scope_request = +type arguments_scope_discharge_request = | ArgsScopeAuto - | ArgsScopeManual of bool + | ArgsScopeManual + | ArgsScopeNoDischarge let load_arguments_scope _ (_,(_,r,scl)) = List.iter (option_iter check_scope) scl; @@ -458,20 +459,18 @@ let cache_arguments_scope o = load_arguments_scope 1 o let subst_arguments_scope (_,subst,(req,r,scl)) = - (None,fst (subst_global subst r),scl) + (ArgsScopeNoDischarge,fst (subst_global subst r),scl) let discharge_arguments_scope (_,(req,r,l)) = - match req,r with - | _, VarRef _ -> None - | Some (ArgsScopeManual true),_ -> None - | _ -> Some (req,pop_global_reference r,l) + if req = ArgsScopeNoDischarge then None + else Some (req,pop_global_reference r,l) let rebuild_arguments_scope (req,r,l) = match req with - | None | Some (ArgsScopeManual true) -> assert false - | Some ArgsScopeAuto -> + | ArgsScopeNoDischarge -> assert false + | ArgsScopeAuto -> (req,r,compute_arguments_scope (Global.type_of_global r)) - | Some (ArgsScopeManual false) -> + | 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 @@ -491,8 +490,10 @@ let (inArgumentsScope,outArgumentsScope) = let declare_arguments_scope_gen req r scl = Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) -let declare_arguments_scope local r scl = - declare_arguments_scope_gen (Some (ArgsScopeManual local)) r scl +let declare_arguments_scope local ref scl = + let req = + if local or isVarRef ref then ArgsScopeNoDischarge else ArgsScopeManual in + declare_arguments_scope_gen req ref scl let find_arguments_scope r = try Refmap.find r !arguments_scope @@ -500,8 +501,8 @@ let find_arguments_scope r = let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope_gen (Some ArgsScopeAuto) ref - (compute_arguments_scope t) + let req = if isVarRef ref then ArgsScopeNoDischarge else ArgsScopeAuto in + declare_arguments_scope_gen req ref (compute_arguments_scope t) (********************************) (* Encoding notations as string *) diff --git a/library/impargs.ml b/library/impargs.ml index 296e53310..fc247f8c1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -418,9 +418,9 @@ let declare_mib_implicits kn = let declare_manual_implicits local ref l = let flags = !implicit_args,!strict_implicit_args,!contextual_implicit_args in let l' = compute_manual_implicits flags ref l in - let local = local or (match ref with VarRef _ -> true | _ -> false) in let req = - if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplManual l) + if local or isVarRef ref then ImplNoDischarge + else ImplInteractive(ref,flags,ImplManual l) in add_anonymous_leaf (inImplicits (req,[ref,l'])) diff --git a/library/libnames.ml b/library/libnames.ml index d951b616e..dcdd5ac41 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -21,6 +21,8 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor +let isVarRef = function VarRef _ -> true | _ -> false + let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> diff --git a/library/libnames.mli b/library/libnames.mli index 2d5d5258f..fe5033d73 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -23,6 +23,8 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor +val isVarRef : global_reference -> bool + val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) |