diff options
Diffstat (limited to 'vernac/declareDef.ml')
| -rw-r--r-- | vernac/declareDef.ml | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index bdda3314ca..652dbf0858 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -14,27 +14,13 @@ open Entries open Globnames open Impargs -let warn_local_declaration = - CWarnings.create ~name:"local-declaration" ~category:"scope" - Pp.(fun (id,kind) -> - Names.Id.print id ++ strbrk " is declared as a local " ++ str kind) - -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_declaration (id,kind); - true -| Local -> true -| Global -> false - let declare_definition ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with - | Discharge when Lib.sections_are_opened () -> + | Discharge -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in VarRef ident - | Discharge | Local | Global -> - let local = get_locality ident ~kind:"definition" local in + | Global local -> let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = Declare.declare_univ_binders gr pl in |