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

val lookup_renamed : t -> Names.Id.t -> EConstr.constr

Lookup the ident in the context that would be used for an evar in this environment, producing a term (Var or Rel) valid in renamed_env.

hide_variable env id tells to hide the binding of id in the ltac environment part of env. 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.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