diff options
| author | Gaëtan Gilbert | 2019-10-13 16:32:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | c3479eceb8e07b37570a80bca9937e3520c61024 (patch) | |
| tree | 136a1773ad9b1bd1cdecd3db26ca0cc64f4516cf /vernac/locality.ml | |
| parent | 26e8b5a545bcf2209d56494ccf4afe143f761fd7 (diff) | |
Use kernel info from Global for Lib.sections_{depth,are_opened}
Diffstat (limited to 'vernac/locality.ml')
| -rw-r--r-- | vernac/locality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/locality.ml b/vernac/locality.ml index f033d32874..5862f51b43 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge = match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) | None, NoDischarge -> Global Declare.ImportDefaultBehavior - | None, DoDischarge when not (Lib.sections_are_opened ()) -> + | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); Global Declare.ImportNeedQualified @@ -55,7 +55,7 @@ let enforce_locality locality_flag = Local in sections is the default, Local not in section forces non-export *) let make_section_locality = - function Some b -> b | None -> Lib.sections_are_opened () + function Some b -> b | None -> Global.sections_are_opened () let enforce_section_locality locality_flag = make_section_locality locality_flag @@ -68,7 +68,7 @@ let enforce_section_locality locality_flag = let make_module_locality = function | Some false -> - if Lib.sections_are_opened () then + if Global.sections_are_opened () then CErrors.user_err Pp.(str "This command does not support the Global option in sections."); false |