From bde492270970223482c77ac1605590b03720e613 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 16 Feb 2015 20:38:01 +0100 Subject: Comment on the unsafe_ functions in Global. --- library/global.mli | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'library') diff --git a/library/global.mli b/library/global.mli index af23d9b72..ebf701acd 100644 --- a/library/global.mli +++ b/library/global.mli @@ -116,11 +116,23 @@ val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool +(** Returns the type of the constant in its global or local universe context. + The type should not be used without pushing it's universe context in + the environmnent of usage. For non-universe-polymorphic constants, it + does not matter. *) + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types Univ.in_universe_context + +(** Returns the type of the constant, forgetting its universe context if + it is polymorphic, use with care: for polymorphic constants, the type + cannot be used to produce a term used by the kernel. + For safe handling of polymorphic global references, one needs an + accompanying [evar_map], see [Evd.fresh_global] and [Evarutil.new_global]. *) + val type_of_global_unsafe : Globnames.global_reference -> Constr.types -(** Returns the universe context of the global reference (whatever it's polymorphic status is). *) +(** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.universe_context (** {6 Retroknowledge } *) -- cgit v1.2.3