package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.proofs/Proof/index.html
Module Proof
Source
type data = {
sigma : Evd.evar_map;
(*A representation of the evar_map
*)EJGA wouldn't it better to just return the proofview?
goals : Evar.t list;
(*Focused goals
*)entry : Proofview.entry;
(*Entry for the proofview
*)stack : (Evar.t list * Evar.t list) list;
(*A representation of the focus stack
*)name : Names.Id.t;
(*The name of the theorem whose proof is being constructed
*)poly : bool;
(*polymorphism
*)
}
val start :
name:Names.Id.t ->
poly:bool ->
?typing_flags:Declarations.typing_flags ->
Evd.evar_map ->
(Environ.env * EConstr.types) list ->
t
val dependent_start :
name:Names.Id.t ->
poly:bool ->
?typing_flags:Declarations.typing_flags ->
Proofview.telescope ->
t
update_sigma_univs
lifts UState.update_sigma_univs
to the proof
val run_tactic :
Environ.env ->
'a Proofview.tactic ->
t ->
t * (bool * Proofview_monad.Info.tree) * 'a
solve (SelectNth n) tac
applies tactic tac
to the n
th subgoal of the current focused proof. solve SelectAll tac
applies tac
to all subgoals.
val solve :
?with_end_tac:unit Proofview.tactic ->
Goal_select.t ->
int option ->
unit Proofview.tactic ->
t ->
t * bool
Option telling if unification heuristics should be used.
val refine_by_tactic :
name:Names.Id.t ->
poly:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.types ->
unit Proofview.tactic ->
Constr.constr * Evd.evar_map
A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other evars solved by side-effects are NOT purged, so that unexpected failures may occur. Ideally all code using this function should be rewritten in the monad.
Helpers to obtain proof state when in an interactive proof
get_proof_context ()
gets the goal context for the first subgoal of the proof