Module Proofview.Goal
val concl : t -> EConstr.constr
concl
,hyps
,env
andsigma
given a goalgl
return respectively the conclusion ofgl
, the hypotheses ofgl
, the environment ofgl
(i.e. the global environment and the hypotheses) and the current evar map.
val hyps : t -> EConstr.named_context
val env : t -> Environ.env
val sigma : t -> Evd.evar_map
val state : t -> Proofview_monad.StateStore.t
val enter : (t -> unit tactic) -> unit tactic
enter t
applies the goal-dependent tactict
in each goal independently, in the manner oftclINDEPENDENT
except that the current goal is also given as an argument tot
.
val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
Like
enter
, but assumes exactly one goal under focus, raising a fatal error otherwise.
val goals : t tactic list tactic
Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type.