From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- library/global.mli | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'library/global.mli') 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 -- cgit v1.2.3