Module Typing

This module provides the typing machine with existential variables and universes.

val type_of : ?refresh:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.types

Typecheck a term and return its type + updated evars, optionally refreshing universes

Typecheck a type and return its sort

Typecheck a term has a given type (assuming the type is OK)

val type_of_variable : Environ.env -> Names.variable -> EConstr.types

Type of a variable.

Solve existential variables using typing

Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate)

val check_type_fixpoint : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Name.t EConstr.binder_annot array -> EConstr.types array -> EConstr.unsafe_judgment array -> Evd.evar_map

Raise an error message if bodies have types not unifiable with the expected ones

Variant of check that assumes that the argument term is well-typed.

val judge_of_sprop : EConstr.unsafe_judgment
val judge_of_prop : EConstr.unsafe_judgment
val judge_of_set : EConstr.unsafe_judgment
val judge_of_variable : Environ.env -> Names.Id.t -> EConstr.unsafe_judgment
val judge_of_float : Environ.env -> Float64.t -> EConstr.unsafe_judgment
val judge_of_string : Environ.env -> Pstring.t -> EConstr.unsafe_judgment

hack

type ('constr, 'types, 'r) bad_relevance =
| BadRelevanceBinder of 'r * ('constr, 'types, 'r) Context.Rel.Declaration.pt
| BadRelevanceCase of 'r * 'constr

Template typing