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.

2 files changed, 11 insertions, 10 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index cc6f29f756..7de92ded59 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -39,7 +39,7 @@ type constant_obj = {
   cst_decl : Cooking.recipe option;
   (** Non-empty only when rebuilding a constant after a section *)
   cst_kind : logical_kind;
-  cst_locl : bool;
+  cst_locl : import_status;
 }
 
 type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
@@ -63,8 +63,9 @@ let cooking_info segment =
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn), obj) =
   (* Never open a local definition *)
-  if obj.cst_locl then ()
-  else
+  match obj.cst_locl with
+  | ImportNeedQualified -> ()
+  | ImportDefaultBehavior ->
     let con = Global.constant_of_delta_kn kn in
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
@@ -137,7 +138,7 @@ let register_constant kn kind local =
   update_tables kn
 
 let register_side_effect (c, role) =
-  let () = register_constant c (IsProof Theorem) false in
+  let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in
   match role with
   | Subproof -> ()
   | Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
@@ -175,7 +176,7 @@ let define_constant ?role ?(export_seff=false) id cd =
   let kn, eff = Global.add_constant ?role ~in_section id decl in
   kn, eff, export
 
-let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = ImportDefaultBehavior) id ?(export_seff=false) (cd, kind) =
   let () = check_exists id in
   let kn, _eff, export = define_constant ~export_seff id cd in
   (* Register the libobjects attached to the constants and its subproofs *)
@@ -183,14 +184,14 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
   let () = register_constant kn kind local in
   kn
 
-let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) =
+let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = ImportDefaultBehavior) id (cd, kind) =
   let kn, eff, export = define_constant ~role id cd in
   let () = assert (List.is_empty export) in
   let () = register_constant kn kind local in
   kn, eff
 
 let declare_definition ?(internal=UserIndividualRequest)
-  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
+  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior)
   id ?types (body,univs) =
   let cb =
     definition_entry ?types ~univs ~opaque body
diff --git a/interp/declare.mli b/interp/declare.mli
index 0b1a396a34..4120a82ca0 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -53,14 +53,14 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   internal specify if the constant has been created by the kernel or by the
   user, and in the former case, if its errors should be silent *)
 val declare_constant :
- ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
+ ?internal:internal_flag -> ?local:import_status -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t
 
 val declare_private_constant :
-  role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
+  role:side_effect_role -> ?internal:internal_flag -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> Id.t -> ?types:constr ->
+  ?local:import_status -> Id.t -> ?types:constr ->
   constr Entries.in_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we