Module Evarutil

new_meta is a generator of unique meta variables

Create a new Type existential variable, as we keep track of them during type-checking and unification.

Create a fresh evar in a context different from its definition context: new_evar_instance sign evd ty inst creates a new evar of context sign and type ty, inst is a mapping of the evar context to the context where the evar should occur. This means that the terms of inst are typed in the occurrence context and their type (seen as a telescope) is sign

head_evar c returns the head evar of c if any

may raise NoHeadEvar

gather_dependent_evars evm seeds classifies the evars in evm as dependent_evars and goals (these may overlap). A goal is an evar in seeds or an evar appearing in the (partial) definition of a goal. A dependent evar is an evar appearing in the type (hypotheses and conclusion) of a goal, or in the type or (partial) definition of a dependent evar. The value return is a map associating to each dependent evar None if it has no (partial) definition or Some s if s is the list of evars appearing in its (partial) definition.

advance sigma g returns Some g' if g' is undefined and is the current avatar of g (for instance g was changed by clear into g'). It returns None if g has been (partially) solved.

occur_evar_upto sigma k c returns true if k appears in c. It looks up recursively in sigma for the value of existential variables.

Replacing all evars, possibly raising Uninstantiated_evar

finalize env sigma f combines universe minimisation, evar-and-universe normalisation and universe restriction.

It minimizes universes in sigma, calls f a normalisation function with respect to the updated sigma and restricts the local universes of sigma to those encountered while running f.

Note that the normalizer passed to f holds some imperative state in its closure.

Like Constr.kind except that kind_of_term sigma t exposes t as an evar e only if e is uninstantiated in sigma. Otherwise the value of e in sigma is (recursively) used.

eq_constr_univs_test ~evd ~extended_evd t u tests equality of t and u up to existential variable instantiation and equalisable universes. The term t is interpreted in evd while u is interpreted in extended_evd. The universe constraints in extended_evd are assumed to be an extension of those in evd.

compare_cumulative_instances cv_pb variance u1 u2 sigma Returns Inl sigma' where sigma' is sigma augmented with universe constraints such that u1 cv_pb? u2 according to variance. Additionally flexible universes in irrelevant positions are unified if possible. Returns Inr p when the former is impossible.

We should only compare constructors at convertible types, so this is only an opportunity to unify universes.

Unification problems

add_unification_pb ?tail pb sigma Add a unification problem pb to sigma, if not already present. Put it at the end of the list if tail is true, by default it is false.