Module DeclareObl

type 'a obligation_body =
| DefinedObl of 'a
| TermObl of Constr.constr
type obligation = {
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;
}
type obligations = obligation array * int
type fixpoint_kind =
| IsFixpoint of Names.lident option list
| IsCoFixpoint
type program_info = {
prg_name : Names.Id.t;
prg_body : Constr.constr;
prg_type : Constr.constr;
prg_ctx : UState.t;
prg_univdecl : UState.universe_decl;
prg_obligations : obligations;
prg_deps : Names.Id.t list;
prg_fixkind : fixpoint_kind option;
prg_implicits : Impargs.manual_implicits;
prg_notations : Vernacexpr.decl_notation list;
prg_poly : bool;
prg_scope : DeclareDef.locality;
prg_kind : Decls.definition_object_kind;
prg_reduce : Constr.constr -> Constr.constr;
prg_hook : DeclareDef.Hook.t option;
prg_opaque : bool;
}
val declare_obligation : program_info -> obligation -> Constr.types -> Constr.types option -> Entries.universes_entry -> bool * obligation

declare_obligation Save an obligation

module ProgMap : CMap.ExtS with type key = Names.Id.t and module Set := Names.Id.Set
val declare_definition : program_info -> Names.GlobRef.t
type progress =
| Remain of int
| Dependent
| Defined of Names.GlobRef.t
type obligation_qed_info = {
name : Names.Id.t;
num : int;
auto : Names.Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress;
}
val obligation_terminator : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit

obligation_terminator part 2 of saving an obligation

val update_obls : program_info -> obligation array -> int -> progress

update_obls prg obls n progress What does this do?

val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t
val program_tcc_summary_tag : program_info CEphemeron.key Names.Id.Map.t Summary.Dyn.tag
val obl_substitution : bool -> obligation array -> Int.Set.t -> (ProgMap.key * (Constr.types * Constr.types)) list
val dependencies : obligation array -> int -> Int.Set.t
val err_not_transp : unit -> unit
val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit
val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t