Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 16 insertions, 2 deletions

diff --git a/library/global.mli b/library/global.mli
index af23d9b7..62d7ea32 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -118,9 +118,23 @@ val is_template_polymorphic : Globnames.global_reference -> bool
 
 val type_of_global_in_context : Environ.env -> 
   Globnames.global_reference -> Constr.types Univ.in_universe_context
-val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
+(** 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. *)
 
-(** Returns the universe context of the global reference (whatever it's polymorphic status is). *)
+val type_of_global_unsafe : Globnames.global_reference -> Constr.types 
+(** 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 should look at a
+    particular instantiation of the reference, in some particular
+    universe context (part of an [env] or [evar_map]), see
+    e.g. [type_of_constant_in]. If you want to create a fresh instance
+    of the reference and get its type look at [Evd.fresh_global] or
+    [Evarutil.new_global] and [Retyping.get_type_of]. *)
+
+(** 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 } *)