# Module `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`

`val nf_enter : (t -> unit tactic) -> unit tactic`

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

. The goal is normalised with respect to evars.

`val enter : (t -> unit tactic) -> unit tactic`

Like

`nf_enter`

, but does not normalize the goal beforehand.

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