diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/global.mli b/library/global.mli index b82039a0c..57e173cb9 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,26 +123,26 @@ 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 -val is_type_in_type : Globnames.global_reference -> bool +val is_polymorphic : GlobRef.t -> bool +val is_template_polymorphic : GlobRef.t -> bool +val is_type_in_type : GlobRef.t -> bool val constr_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its 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.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its 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 its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.AUContext.t +val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) |