Module Evar_refiner

type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr
val w_refine : (Evar.t * Evd.evar_info) -> glob_constr_ltac_closure -> Environ.env -> Evd.evar_map -> Evd.evar_map