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