diff options
| author | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-26 13:50:12 +0200 |
| commit | 27266c1f79e565a6a19da4c79fc1ce83f748e31c (patch) | |
| tree | 865bd07aa81debed13d6c5b5f4b5b2d8d26d7443 /kernel/typeops.mli | |
| parent | 69cbb9c09d5a440461b945c6690745b444649fda (diff) | |
| parent | 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 (diff) | |
Merge PR #8687: Mini reorganization type of global constr of global
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 57acdfe4b5..1fd070d9d5 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -54,11 +54,10 @@ val type_of_variable : env -> variable -> types val judge_of_variable : env -> variable -> unsafe_judgment (** {6 type of a constant } *) - +val type_of_constant_in : env -> pconstant -> types val judge_of_constant : env -> pconstant -> unsafe_judgment (** {6 type of an applied projection } *) - val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) @@ -89,9 +88,7 @@ val judge_of_cast : unsafe_judgment (** {6 Inductive types. } *) - val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -99,7 +96,25 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_constant_in : env -> pconstant -> types +(** {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 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 *) val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit |