new_meta is a generator of unique meta variables

Alias of Evd.new_pure_evar

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

head_evar c returns the head evar of c if any

may raise NoHeadEvar

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.

reachable_from_evars sigma seeds computes the descendents of evars in seeds by restriction or evar-evar unifications in sigma.

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.

But what about qualities?

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.