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 :
EConstr.constr ->
l2r:bool ->
?check_type:(EConstr.types -> bool) ->
(Coq.Rewrite.hypinfo -> Proof_type.tactic) -> Proof_type.tactic
val build :
Coq.Rewrite.hypinfo ->
(int * EConstr.constr) list ->
(EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
val build_with_evar :
Coq.Rewrite.hypinfo ->
(int * EConstr.constr) list ->
(EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
val rewrite :
?abort:bool ->
Coq.Rewrite.hypinfo ->
(int * EConstr.constr) list ->
(Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
end