GlobEnv
Type of environment extended with naming and ltac interpretation data
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
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
val make : hypnaming:Evarutil.naming_mode -> Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> t
Export the underlying environment
val env : t -> Environ.env
val renamed_env : t -> Environ.env
val lfun : t -> Ltac_pretype.unbound_ltac_var_map
val vars_of_env : t -> Names.Id.Set.t
Push to the environment, returning the declaration(s) with interpreted names
val push_rel : hypnaming:Evarutil.naming_mode -> Evd.evar_map -> EConstr.rel_declaration -> t -> EConstr.rel_declaration * t
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 new_evar : t -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?naming:Namegen.intro_pattern_naming_expr -> ?relevance:EConstr.ERelevance.t -> EConstr.constr -> Evd.evar_map * EConstr.constr
val new_type_evar : t -> Evd.evar_map -> src:Evar_kinds.t Loc.located -> Evd.evar_map * EConstr.constr
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
val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> Evd.evar_map * EConstr.unsafe_judgment) -> t -> Evd.evar_map -> Names.Id.t -> Evd.evar_map * EConstr.unsafe_judgment
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
val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> Genarg.glob_generic_argument -> EConstr.unsafe_judgment * Evd.evar_map