package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.vernac/Declare/Obls/index.html
Module Declare.OblsSource
Check obligations are properly solved before closing the what_for section / module
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_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 try_solve_obligations :
pm:OblState.t ->
Names.Id.t option ->
unit Proofview.tactic option ->
OblState.t