package rocq-runtime

  1. Overview
  2. Docs

Module Rewrite.ResultSource

Sourcetype t
Sourcetype rewrite_result_info = {
  1. rew_rel : EConstr.constr;
  2. rew_to : EConstr.constr;
  3. rew_prf : EConstr.constr;
}
Sourceval fail : t
Sourceval identity : t
Sourceval success : rewrite_result_info -> t
Sourceval subst : Evd.evar_map -> (Names.Id.t -> EConstr.constr) -> t -> t