Declare.Oblsval check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unitCheck obligations are properly solved before closing the what_for section / module
val default_tactic : unit Proofview.tactic Stdlib.reftype 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
val prepare_obligations : name:Names.Id.t -> ?types:EConstr.t -> body:EConstr.t -> Environ.env -> Evd.evar_map -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_name_lifter * RetrieveObl.obligation_infoPrepare API, to be removed once we provide the corresponding 1-step API
val add_definition : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t -> opaque:bool -> uctx:UState.t -> ?body:Constr.t ->
?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?using:Vernacexpr.section_subset_expr -> ?obl_hook:OblState.t Hook.g -> RetrieveObl.obligation_info -> OblState.t * progressStart 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 : pm:OblState.t -> info:Info.t -> cinfo:Constr.types CInfo.t list -> opaque:bool -> uctx:UState.t ->
bodies:Constr.t list -> possible_guard:Pretyping.possible_guard -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?using:Vernacexpr.section_subset_expr ->
?obl_hook:OblState.t Hook.g -> RetrieveObl.obligation_info list -> OblState.tStart 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) -> pm:OblState.t -> Genarg.glob_generic_argument option -> Proof.tImplementation of the Obligation command
val next_obligation : pm:OblState.t -> ?final:bool -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.tImplementation of the Next Obligation and Final Obligation commands
val solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progressImplementation of the Solve Obligation command
val solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.tval try_solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.tval show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unitval show_term : pm:OblState.t -> Names.Id.t option -> Pp.tval admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t