`Proofview.Goal`

`val concl : t -> EConstr.constr`

`concl`

, `hyps`

, `env`

and `sigma`

given a goal `gl`

return respectively the conclusion of `gl`

, the hypotheses of `gl`

, the environment of `gl`

(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`

`enter t`

applies the goal-dependent tactic `t`

in each goal independently, in the manner of `tclINDEPENDENT`

except that the current goal is also given as an argument to `t`

.

Like `enter`

, but assumes exactly one goal under focus, raising a fatal error otherwise.

Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type.

`unsolved g`

is `true`

if `g`

is still unsolved in the current proof state.