Module DeclareObl

type 'a obligation_body =
| DefinedObl of 'a
| TermObl of Constr.constr
module Obligation : sig ... end
type obligations = {
obls : Obligation.t array;
remaining : int;
}
type fixpoint_kind =
| IsFixpoint of Names.lident option list
| IsCoFixpoint
module ProgramDecl : sig ... end
val declare_obligation : ProgramDecl.t -> Obligation.t -> Constr.types -> Constr.types option -> Entries.universes_entry -> bool * Obligation.t

declare_obligation Save an obligation

module ProgMap : CMap.ExtS with type key = Names.Id.t and module Set := Names.Id.Set
val declare_definition : ProgramDecl.t -> Names.GlobRef.t
type progress =
| Remain of int

n obligations remaining

| Dependent

Dependent on other definitions

| Defined of Names.GlobRef.t

Defined as id

Resolution status of a program

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, proof mode

val obligation_hook : ProgramDecl.t -> Obligation.t -> Int.t -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) -> Declare.Hook.S.t -> unit

obligation_hook part 2 of saving an obligation, non-interactive mode

val update_obls : ProgramDecl.t -> Obligation.t array -> int -> progress

update_obls prg obls n progress What does this do?

val check_can_close : Names.Id.t -> unit

Check obligations are properly solved before closing a section

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