sig
  type hypinfo = {
    hyp : EConstr.constr;
    hyptype : EConstr.constr;
    context : EConstr.rel_context;
    body : EConstr.constr;
    rel : Coq.Relation.t;
    left : EConstr.constr;
    right : EConstr.constr;
    l2r : bool;
  }
  val get_hypinfo :
    Environ.env ->
    Evd.evar_map ->
    ?check_type:(EConstr.types -> bool) ->
    EConstr.constr -> l2r:bool -> Coq.Rewrite.hypinfo
  val build :
    Coq.Rewrite.hypinfo -> (int * EConstr.constr) list -> EConstr.constr
  val rewrite :
    ?abort:bool ->
    Coq.Rewrite.hypinfo ->
    (int * EConstr.constr) list -> unit Proofview.tactic
end