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)

Type of a variable.

Returns the instantiated type of a metavariable

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)

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