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