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; }