Module `GlobEnv`

type t

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

val make : hypnaming:Evarutil.naming_mode -> Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> t

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

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 Context.binder_annot array * EConstr.constr array) -> t -> Names.Name.t Context.binder_annot array * t

val new_evar : t -> Evd.evar_map -> ?⁠src:Evar_kinds.t Loc.located -> ?⁠naming:Namegen.intro_pattern_naming_expr -> 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

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

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

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

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