Module Declare.Obls
type fixpoint_kind
=
|
IsFixpoint of Names.lident option list
|
IsCoFixpoint
val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit
Check obligations are properly solved before closing the
what_for
section / module
val default_tactic : unit Proofview.tactic Stdlib.ref
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
val prepare_obligation : name:Names.Id.t -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
Prepare API, to be removed once we provide the corresponding 1-step API
val add_definition : pm:OblState.t -> cinfo:Constr.types CInfo.t -> info:Info.t -> ?obl_hook:OblState.t Hook.g -> ?term:Constr.t -> uctx:UState.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?opaque:bool -> RetrieveObl.obligation_info -> OblState.t * 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 byRetrieveObl
It will return whether all the obligations were solved; if so, it will also registerc
with the kernel.
val add_mutual_definitions : (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list -> pm:OblState.t -> info:Info.t -> ?obl_hook:OblState.t Hook.g -> uctx:UState.t -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.t -> Constr.t) -> ?opaque:bool -> ntns:Vernacexpr.decl_notation list -> fixpoint_kind -> OblState.t
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) -> pm:OblState.t -> Genarg.glob_generic_argument option -> Proof.t
Implementation of the
Obligation
command
val next_obligation : pm:OblState.t -> Names.Id.t option -> Genarg.glob_generic_argument option -> Proof.t
Implementation of the
Next Obligation
command
val solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t * progress
Implementation of the
Solve Obligation
command
val solve_all_obligations : pm:OblState.t -> unit Proofview.tactic option -> OblState.t
val try_solve_obligation : pm:OblState.t -> int -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
Number of remaining obligations to be solved for this program
val try_solve_obligations : pm:OblState.t -> Names.Id.t option -> unit Proofview.tactic option -> OblState.t
val show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit
val show_term : pm:OblState.t -> Names.Id.t option -> Pp.t
val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t
val check_program_libraries : unit -> unit