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, 1 insertions, 1 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 1e582e6456..eb8161c2bb 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -7,7 +7,7 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
 
 let declare_definition ~poly ident sigma body =
-  let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
+  let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in
   let udecl = UState.default_univ_decl in
   edeclare ident k ~opaque:false sigma udecl body None []