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
Evar_refinertype glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constrval w_refine : (Evar.t * Evd.evar_info) -> glob_constr_ltac_closure -> Environ.env -> Evd.evar_map -> Evd.evar_map