diff options
| author | Hugo Herbelin | 2018-10-09 20:46:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 16:52:55 +0200 |
| commit | 09d0ba708a96125632344f2f994b45e9075fc303 (patch) | |
| tree | 73cb5365417f4ac92c958e66aa61bab766ba44ec /kernel/typeops.mli | |
| parent | df6b72e348543a289a2ef3f89f32c905add564bc (diff) | |
Moving Global.constr_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.
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e83c1b3dc5..1fd070d9d5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -106,6 +106,14 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t usage. For non-universe-polymorphic constants, it does not matter. *) +(** {6 Building a term from a global reference *) + +(** Map a global reference to a term in its local universe + context. The term 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 constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t + (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) |