Module Obligations

Solving of obligations: Solved obligations are stored as regular global declarations in the global environment, usually with name constant_obligation_number where constant is the original constant and number is the corresponding (internal) number.

Solving an obligation can trigger a bit of a complex cascaded callback path; closing an obligation can indeed allow all other obligations to be closed, which in turn may trigged the declaration of the original constant. Care must be taken, as this can modify Global.env in arbitrarily ways. Current code takes some care to refresh the env in the proper boundaries, but the invariants remain delicate.

Saving of obligations: as open obligations use the regular proof mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason obligations code is split in two: this file, Obligations, taking care of the top-level vernac commands, and DeclareObl, which is called by `Lemmas` to close an obligation proof and eventually to declare the top-level Programed constant.

There is little obligations-specific code in DeclareObl, so eventually that file should be integrated in the regular Declare path, as it gains better support for "dependent_proofs".

val default_tactic : unit Proofview.tactic Stdlib.ref
val add_definition : name:Names.Id.t -> ?⁠term:Constr.constr -> Constr.types -> uctx:UState.t -> ?⁠udecl:UState.universe_decl -> ?⁠impargs:Impargs.manual_implicits -> poly:bool -> ?⁠scope:Declare.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠tactic:unit Proofview.tactic -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Declare.Hook.t -> ?⁠opaque:bool -> RetrieveObl.obligation_info -> DeclareObl.progress

Start a Program Definition c proof. uctx udecl impargs kind scope poly etc... come from the interpretation of the vernacular; `obligation_info` was generated by RetrieveObl It will return whether all the obligations were solved; if so, it will also register c with the kernel.

val add_mutual_definitions : (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?⁠udecl:UState.universe_decl -> ?⁠tactic:unit Proofview.tactic -> poly:bool -> ?⁠scope:Declare.locality -> ?⁠kind:Decls.definition_object_kind -> ?⁠reduce:(Constr.constr -> Constr.constr) -> ?⁠hook:Declare.Hook.t -> ?⁠opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit

Start a Program Fixpoint declaration, similar to the above, except it takes a list now.

val obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> Lemmas.t

Implementation of the Obligation command

val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t

Implementation of the Next Obligation command

val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress

Implementation of the Solve Obligation command

val solve_all_obligations : unit Proofview.tactic option -> unit
val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit

Number of remaining obligations to be solved for this program

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