From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. --- library/global.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'library/global.mli') diff --git a/library/global.mli b/library/global.mli index 015f4d582..906d246ee 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 } *) -- cgit v1.2.3