diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /toplevel/locality.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'toplevel/locality.ml')
-rw-r--r-- | toplevel/locality.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/toplevel/locality.ml b/toplevel/locality.ml index ef789aa5..154f787e 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -18,7 +18,7 @@ let check_locality locality_flag = match locality_flag with | Some b -> let s = if b then "Local" else "Global" in - Errors.errorlabstrm "Locality.check_locality" + CErrors.errorlabstrm "Locality.check_locality" (str "This command does not support the \"" ++ str s ++ str "\" prefix.") | None -> () @@ -26,17 +26,22 @@ let check_locality locality_flag = (* Commands which supported an inlined Local flag *) +let warn_deprecated_local_syntax = + CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated" + (fun () -> + Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.") + let enforce_locality_full locality_flag local = let local = match locality_flag with | Some false when local -> - Errors.error "Cannot be simultaneously Local and Global." + CErrors.error "Cannot be simultaneously Local and Global." | Some true when local -> - Errors.error "Use only prefix \"Local\"." + CErrors.error "Use only prefix \"Local\"." | None -> if local then begin - Pp.msg_warning (Pp.str "Obsolete syntax: use \"Local\" as a prefix."); - Some true + warn_deprecated_local_syntax (); + Some true end else None | Some b -> Some b in @@ -61,7 +66,7 @@ let enforce_locality_exp locality_flag local = | None, Some local -> local | Some b, None -> local_of_bool b | None, None -> Decl_kinds.Global - | Some _, Some _ -> Errors.error "Local non allowed in this case" + | Some _, Some _ -> CErrors.error "Local non allowed in this case" (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -82,7 +87,7 @@ let enforce_section_locality locality_flag local = let make_module_locality = function | Some false -> if Lib.sections_are_opened () then - Errors.error + CErrors.error "This command does not support the Global option in sections."; false | Some true -> true |