diff options
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 36 |
1 files changed, 24 insertions, 12 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index bff40b017f..4193324136 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -12,7 +12,6 @@ open Names open Constr open Univ open Environ -open Entries (** {6 Typing functions (not yet tagged as safe) } @@ -27,8 +26,8 @@ val infer : env -> constr -> unsafe_judgment val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment -val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) +val check_context : + env -> Constr.rel_context -> env (** {6 Basic operations of the typing machine. } *) @@ -43,7 +42,6 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : Sorts.contents -> unsafe_judgment val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) @@ -55,12 +53,11 @@ 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 -> Names.projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) val judge_of_apply : @@ -90,9 +87,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. } *) @@ -100,9 +95,26 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Names.projection puniverses -> types +(** {6 Type of global references. } *) -val type_of_constant_in : env -> pconstant -> types +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 -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> + ('a -> constr) -> 'a -> Constr.named_context -> unit |