Module `Obligations`

val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
val check_evars : Environ.env -> Evd.evar_map -> unit
val evar_dependencies : Evd.evar_map -> Evar.t -> Evar.Set.t
val sort_dependencies : (Evar.t * Evd.evar_info * Evar.Set.t) list -> (Evar.t * Evd.evar_info * Evar.Set.t) list
val eterm_obligations : Environ.env -> Names.Id.t -> Evd.evar_map -> int -> ?⁠status:Evar_kinds.obligation_definition_status -> Constr.constr -> Constr.types -> (Names.Id.t * Constr.types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array * ((Evar.t * Names.Id.t) list * ((Names.Id.t -> Constr.constr) -> Constr.constr -> Constr.constr)) * Constr.constr * Constr.types

type obligation_info = (Names.Id.t * Constr.types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
type progress = | Remain of int | Dependent | Defined of Names.GlobRef.t

val default_tactic : unit Proofview.tactic Stdlib.ref
val add_definition : Names.Id.t -> ?⁠term:Constr.constr -> Constr.types -> UState.t -> ?⁠univdecl:UState.universe_decl -> ?⁠implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?⁠kind:Decl_kinds.definition_kind -> ?⁠tactic:unit Proofview.tactic -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Lemmas.declaration_hook -> ?⁠opaque:bool -> obligation_info -> progress

type notations = (Names.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
type fixpoint_kind = | IsFixpoint of Names.lident option list | IsCoFixpoint

val add_mutual_definitions : (Names.Id.t * Constr.constr * Constr.types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> UState.t -> ?⁠univdecl:UState.universe_decl -> ?⁠tactic:unit Proofview.tactic -> ?⁠kind:Decl_kinds.definition_kind -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Lemmas.declaration_hook -> ?⁠opaque:bool -> notations -> fixpoint_kind -> unit
val obligation : ontop:Proof_global.t option -> (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> Proof_global.t
val next_obligation : ontop:Proof_global.t option -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof_global.t
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
val solve_all_obligations : unit Proofview.tactic option -> unit
val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
val show_obligations : ?⁠msg:bool -> Names.Id.t option -> unit
val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit