Module DeclareObl.Obligation
type t
= private
{
obl_name : Names.Id.t;
obl_type : Constr.types;
obl_location : Evar_kinds.t Loc.located;
obl_body : Constr.pconstant obligation_body option;
obl_status : bool * Evar_kinds.obligation_definition_status;
obl_deps : Int.Set.t;
obl_tac : unit Proofview.tactic option;
}
val set_type : typ:Constr.types -> t -> t
val set_body : body:Constr.pconstant obligation_body -> t -> t