Cleaning the status of Local Definition and similar.

Formerly, knowing if a declaration was to be discharged, to be global
but invisible at import, or to be global but visible at import was
obtained by combining the parser-level information (i.e. use of
Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use
of Local vs Global) with the result of testing whether there were open
sections.

We change the meaning of the Discharge flag: it does not tell anymore
that it was syntactically a Variable/Hypothesis/Let, but tells the
expected semantics of the declaration (issuing a warning in the
parser-to-interpreter step if the semantics is not the one suggested
by the syntax). In particular, the interpretation/command engine
becomes independent of the parser.

The new "semantic" type is:

type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status

In the process, we found a couple of inconsistencies in the treatment
of the locality status. See bug #8722 and test file LocalDefinition.v.

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