diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index caa20b534..ef918ef8d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -142,21 +142,21 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce -let warn_local_let_definition = - CWarnings.create ~name:"local-let-definition" ~category:"scope" - (fun id -> - pr_id id ++ strbrk " is declared as a local definition") +let warn_local_declaration = + CWarnings.create ~name:"local-declaration" ~category:"scope" + (fun (id,kind) -> + pr_id id ++ strbrk " is declared as a local " ++ str kind) -let get_locality id = function +let get_locality id ~kind = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) - warn_local_let_definition id; + warn_local_declaration (id,kind); true | Local -> true | Global -> false let declare_global_definition ident ce local k pl imps = - let local = get_locality ident local in + let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -240,7 +240,7 @@ match local with (r,Univ.Instance.empty,true) | Global | Local | Discharge -> - let local = get_locality ident local in + let local = get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) |