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.

10 files changed, 65 insertions, 79 deletions

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