Rewrite.Resulttype rewrite_result_info = {rew_rel : EConstr.constr;rew_to : EConstr.constr;rew_prf : EConstr.constr;}val fail : tval identity : tval success : rewrite_result_info -> tval subst : Evd.evar_map -> (Names.Id.t -> EConstr.constr) -> t -> t