diff options
| -rw-r--r-- | library/global.mli | 14 |
1 files changed, 13 insertions, 1 deletions
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 } *) |