diff options
| author | Hugo Herbelin | 2018-10-09 20:22:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | df6b72e348543a289a2ef3f89f32c905add564bc (patch) | |
| tree | 3fc74e3474457f12a9cd4975707c67553b3e6db1 /kernel/typeops.mli | |
| parent | 988aab80e03e593c76869b113c5bcc043209d952 (diff) | |
Moving Global.type_of_global_in_context to Typeops.
It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.
Also updated the comments.
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 515e22c99b..e83c1b3dc5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -96,6 +96,16 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment +(** {6 Type of global references. } *) + +val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t +(** Returns the type of the global reference, by creating a fresh + instance of polymorphic references and computing their + instantiated 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. *) + (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) |