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