diff options
Diffstat (limited to 'toplevel/locality.ml')
| -rw-r--r-- | toplevel/locality.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/toplevel/locality.ml b/toplevel/locality.ml index c4c891b89..62aa85160 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -26,6 +26,11 @@ 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 @@ -35,8 +40,8 @@ let enforce_locality_full locality_flag local = Errors.error "Use only prefix \"Local\"." | None -> if local then begin - Feedback.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 |