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.

26 files changed, 159 insertions, 119 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 339ac2d9b7..cc58222fbf 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,6 +5,10 @@
 - Functions and types deprecated in 8.10 have been removed in Coq
   8.11.
 
+- Type Decl_kinds.locality has been restructured, see commit
+  message. Main change to do generally is to change the flag "Global"
+  to "Global ImportDefaultBehavior".
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
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 []
 
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
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 8decdbea1e..39042e1ab7 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -12,7 +12,9 @@
 
 type discharge = DoDischarge | NoDischarge
 
-type locality = Discharge | Local | Global
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
+type locality = Discharge | Global of import_status
 
 type binding_kind = Explicit | Implicit
 
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 9c1882dc9a..7c0f269481 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -26,7 +26,7 @@ let start_deriving f suchthat lemma =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e38ea992ab..b3a799fb6a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,7 +995,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+    Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
     evd
   lemma_type
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7b26cb0c74..965ce68811 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -311,7 +311,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let pstate =
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+      Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
       !evd
       (EConstr.of_constr new_principle_type)
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 241da053b7..7070f01c6f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -417,7 +417,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       ComDefinition.do_definition
         ~program_mode:false
 	fname
-        (Decl_kinds.Global,false,Decl_kinds.Definition) pl
+        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
 	 List.fold_left
@@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
+       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 48cf040919..6d9690096f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -124,26 +124,20 @@ open Declare
 
 let definition_message = Declare.definition_message
 
-let get_locality = function
-| Discharge -> true
-| Local -> true
-| Global -> false
-
 let save id const ?hook uctx (locality,_,kind) =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
-  let l,r = match locality with
-    | Discharge when Lib.sections_are_opened () ->
+  let r = match locality with
+    | Discharge ->
         let k = Kindops.logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef const in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
-	(Local, VarRef id)
-    | Discharge | Local | Global ->
-        let local = get_locality locality in
+        VarRef id
+    | Global local ->
         let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
-	(locality, ConstRef kn)
+        ConstRef kn
   in
-  Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
+  Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
   definition_message id
 
 let with_full_print f a =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 03568fc6c7..8a16326ba3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let pstate = Lemmas.start_proof
 	   lem_id
-           (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
+           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
            !evd
            typ in
          let pstate = fst @@ Pfedit.by
@@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	   i*)
 	 let lem_id = mk_complete_id f_id in
          let pstate = Lemmas.start_proof lem_id
-           (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
+           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
          (fst lemmas_types_infos.(i)) in
          let pstate = fst (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e2321d233c..5bedb360d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1371,7 +1371,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
   in
   let pstate = Lemmas.start_proof
     na
-    (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+    Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
     sigma gls_type ~hook:(Lemmas.mk_hook hook) in
   let pstate = if Indfun_common.is_strict_tcc  ()
   then
@@ -1411,7 +1411,7 @@ let com_terminate
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
     let pstate = Lemmas.start_proof thm_name
-      (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+      (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
       ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
     let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in
     fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
@@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd
+    let pstate = Lemmas.start_proof eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let pstate = fst @@ by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e0a31e7dba..b99e77ab2b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Proof_global.t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
-  let kind = Decl_kinds.Global, atts.polymorphic,
+  let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
              Decl_kinds.DefinitionBody Decl_kinds.Instance
   in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 66b47a64a7..c7fcc66120 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -117,7 +117,7 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   let goals = [ (Global.env_of_context sign , typ) ] in
@@ -139,7 +139,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global, poly, Proof Theorem in
+  let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
   let ce, status, univs =
     build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
   let body = Future.force ce.const_entry_body in
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index a5b2f99457..e91fe5067c 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      question, how does abstract behave when discharge is local for example?
   *)
   let goal_kind, suffix = if opaque
-    then (Global,poly,Proof Theorem), "_subproof"
-    else (Global,poly,DefinitionBody Definition), "_subterm" in
+    then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
+    else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
   let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl
+    Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v
new file mode 100644
index 0000000000..22fb09526d
--- /dev/null
+++ b/test-suite/success/LocalDefinition.v
@@ -0,0 +1,53 @@
+(* Test consistent behavior of Local Definition (#8722) *)
+
+(* Test consistent behavior of Local Definition wrt Admitted *)
+
+Module TestAdmittedVisibility.
+  Module A.
+    Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *)
+    Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *)
+    Local Definition c1 := 0.
+    Local Parameter d1 : nat.
+    Section S.
+      Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *)
+      Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *)
+      Local Definition c2 := 0.
+      Local Parameter d2 : nat.
+    End S.
+  End A.
+  Import A.
+  Fail Check a1. (* used to be accepted *)
+  Fail Check b1. (* used to be accepted *)
+  Fail Check c1.
+  Fail Check d1.
+  Fail Check a2. (* used to be accepted *)
+  Fail Check b2. (* used to be accepted *)
+  Fail Check c2.
+  Fail Check d2.
+End TestAdmittedVisibility.
+
+(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
+
+Module TestVariableAsInstances.
+  Module Test1.
+    Set Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Definition testU := _ : U. (* _ resolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" *)
+    Definition testT := _ : T. (* _ resolved *)
+  End Test1.
+
+  Module Test2.
+    Unset Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Fail Definition testU := _ : U. (* _ unresolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
+    Fail Definition testT := _ : T. (* used to succeed *)
+  End Test2.
+End TestVariableAsInstances.
diff --git a/vernac/class.ml b/vernac/class.ml
index f3a279eab1..58cef5db4f 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -358,9 +358,9 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
 
 let add_coercion_hook poly _uctx _trans local ref =
   let local = match local with
-  | Discharge
-  | Local -> true
-  | Global -> false
+  | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
+  | Global ImportNeedQualified -> true
+  | Global ImportDefaultBehavior -> false
   in
   let () = try_add_new_coercion ref ~local poly in
   let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
@@ -370,9 +370,9 @@ let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
 let add_subclass_hook poly _uctx _trans local ref =
   let stre = match local with
-  | Local -> true
-  | Global -> false
-  | Discharge -> assert false
+  | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
+  | Global ImportNeedQualified -> true
+  | Global ImportDefaultBehavior -> false
   in
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl ~local:stre poly
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9cc8467c57..ed207b52dd 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -367,7 +367,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
   let hook = Lemmas.mk_hook hook in
   let ctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition id ?term:constr
-           ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
+           ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
 
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
@@ -377,7 +377,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
      the refinement manually.*)
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
-  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
   let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
       ~hook:(Lemmas.mk_hook
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 49f32dd401..591e4b130f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -45,7 +45,7 @@ let should_axiom_into_instance = function
 
 let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
 match local with
-| Discharge when Lib.sections_are_opened () ->
+| Discharge ->
   let ctx = match ctx with
     | Monomorphic_entry ctx -> ctx
     | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
@@ -61,9 +61,8 @@ match local with
   let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
   (r,Univ.Instance.empty,true)
 
-| Global | Local | Discharge ->
+| Global local ->
   let do_instance = should_axiom_into_instance kind in
-  let local = DeclareDef.get_locality ident ~kind:"axiom" local in
   let inl = let open Declaremods in match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())
@@ -78,6 +77,7 @@ match local with
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
+  let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
     | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
@@ -124,7 +124,7 @@ let process_assumptions_udecls kind l =
     | (_, ([], _))::_ | [] -> assert false
   in
   let () = match kind, udecl with
-    | (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
+    | (Discharge, _, _), Some _ ->
       let loc = first_id.CAst.loc in
       let msg = Pp.str "Section variables cannot be polymorphic." in
       user_err ?loc  msg
@@ -288,7 +288,9 @@ let context poly l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let decl = (Discharge, poly, Context) in
+      let persistence =
+        if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in
+      let decl = (persistence, poly, Context) in
       let nstatus = match b with
       | None ->
         pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 7a4e6d8698..fd88c6c4ad 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -305,7 +305,7 @@ let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes)
       fixdefs) in
   let evd = Evd.from_ctx ctx in
   let pstate = Lemmas.start_proof_with_initialization
-    (Global,poly, DefinitionBody CoFixpoint)
+    (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint)
     evd pl (Some(true,[],init_tac)) thms None in
   declare_cofixpoint_notations ntns;
   pstate
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
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index c4500d0a6b..2b9d9567cd 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,8 +11,6 @@
 open Names
 open Decl_kinds
 
-val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
-
 val declare_definition
   : Id.t
   -> definition_kind
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d14c7ddf8f..7de6d28560 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -178,18 +178,14 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes
     let k = Kindops.logical_kind_of_goal_kind kind in
     let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
     let r = match locality with
-      | Discharge when Lib.sections_are_opened () ->
+      | Discharge ->
           let c = SectionLocalDef const in
           let _ = declare_variable id (Lib.cwd(), c, k) in
           let () = if should_suggest
             then Proof_using.suggest_variable (Global.env ()) id
           in
           VarRef id
-      | Local | Global | Discharge ->
-          let local = match locality with
-          | Local | Discharge -> true
-          | Global -> false
-          in
+      | Global local ->
           let kn =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           let () = if should_suggest
@@ -213,7 +209,7 @@ let fresh_name_for_anonymous_theorem () =
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
-     locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
@@ -233,16 +229,12 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
           in
           let c = SectionLocalAssum ((t_i, univs),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (Discharge, VarRef id,imps)
-      | Local | Global ->
-          let local = match locality with
-          | Local -> true
-          | Global -> false
-          | Discharge -> assert false
-          in
+          (VarRef id,imps)
+      | Global local ->
+          let k = IsAssumption Conjectural in
           let decl = (ParameterEntry (None,(t_i,univs),None), k) in
           let kn = declare_constant id ~local decl in
-          (locality,ConstRef kn,imps))
+          (ConstRef kn,imps))
   | Some body ->
       let body = norm body in
       let k = Kindops.logical_kind_of_goal_kind kind in
@@ -260,18 +252,13 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (Discharge,VarRef id,imps)
-      | Local | Global ->
-        let local = match locality with
-        | Local -> true
-        | Global -> false
-        | Discharge -> assert false
-        in
+          (VarRef id,imps)
+      | Global local ->
         let const =
           Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
 	in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        (locality,ConstRef kn,imps)
+        (ConstRef kn,imps)
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
@@ -282,17 +269,17 @@ let check_anonymity id save_ident =
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
                    (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
-                                spc () ++ strbrk "declared as an axiom.")
+                                spc () ++ strbrk "declared as a local axiom.")
 
 let admit ?hook ctx (id,k,e) pl () =
-  let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
-  let () = match k with
-  | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
+  let local = match k with
+  | Global local, _, _ -> local
+  | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified
   in
+  let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) pl;
-  call_hook ?hook ctx [] Global (ConstRef kn)
+  call_hook ?hook ctx [] (Global local) (ConstRef kn)
 
 (* Starting a goal *)
 
@@ -380,8 +367,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
             let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
             let env = Global.env () in
             List.map_i (save_remaining_recthms env sigma kind norm uctx body opaq) 1 other_thms in
-        let thms_data = (strength,ref,imps)::other_thms_data in
-        List.iter (fun (strength,ref,imps) ->
+        let thms_data = (ref,imps)::other_thms_data in
+        List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
       let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 21be73b39c..465f04bc6e 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -12,10 +12,9 @@ open Decl_kinds
 
 (** * Managing locality *)
 
-let local_of_bool = function
-  | true -> Local
-  | false -> Global
-
+let importability_of_bool = function
+  | true -> ImportNeedQualified
+  | false -> ImportDefaultBehavior
 
 (** Positioning locality for commands supporting discharging and export
      outside of modules *)
@@ -28,10 +27,22 @@ let make_non_locality = function Some false -> false | _ -> true
 
 let make_locality = function Some true -> true | _ -> false
 
+let warn_local_declaration =
+  CWarnings.create ~name:"local-declaration" ~category:"scope"
+    Pp.(fun () ->
+        Pp.strbrk "Interpreting this declaration as if " ++
+        strbrk "a global declaration prefixed by \"Local\", " ++
+        strbrk "i.e. as a global declaration which shall not be " ++
+        strbrk "available without qualification when imported.")
+
 let enforce_locality_exp locality_flag discharge =
   match locality_flag, discharge with
-  | Some b, NoDischarge -> local_of_bool b
-  | None, NoDischarge -> Global
+  | Some b, NoDischarge -> Global (importability_of_bool b)
+  | None, NoDischarge -> Global ImportDefaultBehavior
+  | None, DoDischarge when not (Lib.sections_are_opened ()) ->
+     (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
+     warn_local_declaration ();
+     Global ImportNeedQualified
   | None, DoDischarge -> Discharge
   | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
   | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 0d93e19723..36cf9e0a31 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -643,7 +643,7 @@ let declare_obligation prg obl body ty uctx =
           const_entry_feedback = None;
       } in
       (* ppedrot: seems legit to have obligations as local *)
-      let constant = Declare.declare_constant obl.obl_name ~local:true
+      let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
 	(DefinitionEntry ce,IsProof Property)
       in
       if not opaque then add_hint (Locality.make_section_locality None) prg constant;
@@ -787,9 +787,11 @@ let dependencies obls n =
       obls;
     !res
 
-let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind poly =
+  Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
 
-let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind poly =
+  Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma)
 
 let kind_of_obligation poly o =
   match o with
@@ -1102,7 +1104,7 @@ let show_term n =
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
 let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+                   ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
@@ -1122,7 +1124,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
-                           ?(kind=Global,false,Definition) ?(reduce=reduce)
+                           ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
@@ -1153,7 +1155,7 @@ let admit_prog prg =
         | None ->
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
-            let kn = Declare.declare_constant x.obl_name ~local:true
+            let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified
               (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 8668f01053..4f66f2b790 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -606,7 +606,7 @@ let vernac_definition_name lid local =
   let () =
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
-    | Local | Global -> Dumpglob.dump_definition lid false "def"
+    | Global _ -> Dumpglob.dump_definition lid false "def"
   in
   lid
 
@@ -658,13 +658,13 @@ let vernac_exact_proof ~pstate c =
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
-  let global = local == Global in
   let kind = local, atts.polymorphic, kind in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
-	if global then Dumpglob.dump_definition lid false "ax"
-	else Dumpglob.dump_definition lid true "var") idl) l;
+          match local with
+            | Global _ -> Dumpglob.dump_definition lid false "ax"
+            | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom