Imported Upstream version 8.5~beta3+dfsg

1 files changed, 8 insertions, 7 deletions

diff --git a/library/global.mli b/library/global.mli
index 62d7ea32..03469bea 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,23 +27,23 @@ val named_context : unit -> Context.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> unit
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def   : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
 
 val add_constant :
-  DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
+  DirPath.t -> Id.t -> Safe_typing.global_declaration ->
+    constant * Safe_typing.exported_private_constant list
 val add_mind :
   DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive
 
 (** Extra universe constraints *)
 val add_constraints : Univ.constraints -> unit
 
-val push_context : Univ.universe_context -> unit
-val push_context_set : Univ.universe_context_set -> unit
+val push_context : bool -> Univ.universe_context -> unit
+val push_context_set : bool -> Univ.universe_context_set -> unit
 
 (** Non-interactive modules and module types *)
 
@@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t ->
   module_path * Safe_typing.compiled_library * Safe_typing.native_library
 val import :
   Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
-  module_path * Nativecode.symbol array
+  module_path
 
 (** {6 Misc } *)
 
@@ -112,6 +112,7 @@ val import :
 val env_of_context : Environ.named_context_val -> Environ.env
 
 val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
+val is_joined_environment : unit -> bool
 
 val is_polymorphic : Globnames.global_reference -> bool
 val is_template_polymorphic : Globnames.global_reference -> bool