Module GlobEnvSource

Type of environment extended with naming and ltac interpretation data

To embed constr in glob_constr

Pretyping name management

The following provides a level of abstraction for the kind of environment used for type inference (so-called pretyping); in particular:

• it supports that term variables can be interpreted as Ltac variables pointing to the effective expected name
• it incrementally and lazily computes the renaming of rel variables used to build purely-named evar contexts

Build a pretyping environment from an ltac environment

Export the underlying environment

Push to the environment, returning the declaration(s) with interpreted names

Declare an evar using renaming information

hide_variable env na id tells to hide the binding of id in the ltac environment part of env and to additionally rebind it to id' in case na is some Name id'. It is useful e.g. for the dual status of y as term and binder. This is the case of match y return p with ... end which implicitly denotes match z as z return p with ... end when y is bound to a variable z and match t as y return p with ... end when y is bound to a non-variable term t. In the latter case, the binding of y to t should be hidden in p.

In case a variable is not bound by a term binder, look if it has an interpretation as a term in the ltac_var_map

Interp an identifier as an ltac variable bound to an identifier, or as the identifier itself if not bound to an ltac variable

Interpreting a generic argument, typically a "ltac:(...)", taking into account the possible renaming