package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.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 * Sorts.relevance list) ->
?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) ->
pm:OblState.t ->
Genarg.glob_generic_argument option ->
Proof.tImplementation of the Obligation n of id with tac command
val next_obligation :
pm:OblState.t ->
?final:bool ->
Names.Id.t option ->
Genarg.glob_generic_argument option ->
Proof.tImplementation of the Next Obligation of id with tac and Final Obligation of id with tac commands
val solve_obligations :
pm:OblState.t ->
Names.Id.t option ->
unit Proofview.tactic option ->
OblState.t * progressImplementation of the Solve Obligations of id with tac command
val try_solve_obligations :
pm:OblState.t ->
Names.Id.t option ->
unit Proofview.tactic option ->
OblState.tImplementation of the Solve All Obligations with tac command
Implementation of the Obligations of id command
Implementation of the Preterm of id command
Implementation of the Admit Obligations of id command
val program_inference_hook :
Environ.env ->
Evd.evar_map ->
Evar.t ->
(Evd.evar_map * EConstr.t) option