Module GlobEnv

Type of environment extended with naming and ltac interpretation data

type t

To embed constr in glob_constr

type 'a obj_interp_fun = ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> 'a -> EConstr.unsafe_judgment * Evd.evar_map
val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit
Pretyping name management

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

Build a pretyping environment from an ltac environment

Export the underlying environment

val env : t -> Environ.env
val renamed_env : t -> Environ.env
val vars_of_env : t -> Names.Id.Set.t

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

val push_rel_context : hypnaming:Evarutil.naming_mode -> ?force_names:bool -> Evd.evar_map -> EConstr.rel_context -> t -> EConstr.rel_context * t
val push_rec_types : hypnaming:Evarutil.naming_mode -> Evd.evar_map -> (Names.Name.t EConstr.binder_annot array * EConstr.constr array) -> t -> Names.Name.t EConstr.binder_annot array * t

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.

val hide_variable : t -> Names.Name.t -> Names.Id.t -> t

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

val interp_ltac_id : t -> Names.Id.t -> Names.Id.t

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