Module Obligations

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
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
val eterm_obligations : Environ.env -> Names.Id.t -> Evd.evar_map -> int -> ?⁠status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> obligation_info * ((Evar.t * Names.Id.t) list * ((Names.Id.t -> EConstr.constr) -> EConstr.constr -> Constr.constr)) * Constr.constr * Constr.types
val default_tactic : unit Proofview.tactic Stdlib.ref
val add_definition : name:Names.Id.t -> ?⁠term:Constr.constr -> Constr.types -> UState.t -> ?⁠univdecl:UState.universe_decl -> ?⁠implicits:Impargs.manual_implicits -> poly:bool -> ?⁠scope:DeclareDef.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠tactic:unit Proofview.tactic -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:DeclareDef.Hook.t -> ?⁠opaque:bool -> obligation_info -> DeclareObl.progress
val add_mutual_definitions : (Names.Id.t * Constr.constr * Constr.types * Impargs.manual_implicits * obligation_info) list -> UState.t -> ?⁠univdecl:UState.universe_decl -> ?⁠tactic:unit Proofview.tactic -> poly:bool -> ?⁠scope:DeclareDef.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:DeclareDef.Hook.t -> ?⁠opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit
val obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> Lemmas.t
val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.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
exception NoObligations of Names.Id.t option
val explain_no_obligations : Names.Id.t option -> Pp.t
val check_program_libraries : unit -> unit