Module Evarutil

new_meta is a generator of unique meta variables

Low-level interface to create an evar.

parameter src

User-facing source for the evar

parameter filter

See Evd.Filter, must be the same length as named_context_val

parameter identity

See Evd.Identity, must be the name projection of named_context_val

parameter naming

A naming scheme for the evar

parameter principal

Whether the evar is the principal goal

parameter named_context_val

The context of the evar

parameter types

The type of conclusion of the 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

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.

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.

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.