aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-19 17:53:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-19 17:53:43 +0200
commit1fda29d0179d60c83ead5db6e3062511aba7d264 (patch)
treec6d274bd98051263f80d471ecb14dff06370b4f0
parentf1a561d847e207433a0ec3e6333798dfa19e4a0c (diff)
Fix warning when using Variables at toplevel.
-rw-r--r--toplevel/command.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 097865648..12c387dcf 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -140,21 +140,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
@@ -238,7 +238,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())