Merge PR #8726: More robust treatment of the Discharge status

Reviewed-by: aspiwack
Ack-by: ejgallego
Reviewed-by: ppedrot

3 files changed, 13 insertions, 11 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
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index a537b4848c..274f9b851a 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -91,7 +91,8 @@ let type_of_logical_kind = function
       (match a with
       | Definitional -> "defax"
       | Logical -> "prfax"
-      | Conjectural -> "prfax")
+      | Conjectural -> "prfax"
+      | Context -> "prfax")
   | IsProof th ->
       (match th with
       | Theorem