Comment on the unsafe_ functions in Global.

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 } *)